pith. machine review for the scientific record. sign in
structure definition def or abbrev

RecognitionAutomorphism

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 148structure RecognitionAutomorphism (r : Recognizer C E) extends RecognitionPreservingMap r where
 149  /-- The inverse function -/
 150  invFun : C → C
 151  /-- Left inverse property -/
 152  left_inv : ∀ c, invFun (toFun c) = c
 153  /-- Right inverse property -/
 154  right_inv : ∀ c, toFun (invFun c) = c
 155
 156/-- The inverse of an automorphism preserves events -/
 157theorem RecognitionAutomorphism.inv_preserves_event (T : RecognitionAutomorphism r) (c : C) :
 158    r.R (T.invFun c) = r.R c := by

proof body

Definition body.

 159  have h := T.preserves_event (T.invFun c)
 160  rw [T.right_inv] at h
 161  exact h.symm
 162
 163/-- The inverse of an automorphism is an automorphism -/
 164def RecognitionAutomorphism.inv (T : RecognitionAutomorphism r) : RecognitionAutomorphism r where
 165  toFun := T.invFun
 166  preserves_event := T.inv_preserves_event
 167  invFun := T.toFun
 168  left_inv := T.right_inv
 169  right_inv := T.left_inv
 170
 171/-- The identity automorphism -/

used by (12)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (24)

Lean names referenced from this declaration's body.