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

compAutomorphism

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)

 180def compAutomorphism (T₁ T₂ : RecognitionAutomorphism r) : RecognitionAutomorphism r where
 181  toFun := T₁.toFun ∘ T₂.toFun

proof body

Definition body.

 182  preserves_event := fun c => by
 183    simp only [Function.comp_apply]
 184    rw [T₁.preserves_event, T₂.preserves_event]
 185  invFun := T₂.invFun ∘ T₁.invFun
 186  left_inv := fun c => by
 187    simp only [Function.comp_apply]
 188    -- Goal: T₂.invFun (T₁.invFun (T₁.toFun (T₂.toFun c))) = c
 189    have h1 : T₁.invFun (T₁.toFun (T₂.toFun c)) = T₂.toFun c := T₁.left_inv _
 190    rw [h1, T₂.left_inv]
 191  right_inv := fun c => by
 192    simp only [Function.comp_apply]
 193    -- Goal: T₁.toFun (T₂.toFun (T₂.invFun (T₁.invFun c))) = c
 194    have h1 : T₂.toFun (T₂.invFun (T₁.invFun c)) = T₁.invFun c := T₂.right_inv _
 195    rw [h1, T₁.right_inv]
 196
 197/-! ## Algebraic Properties of Automorphisms -/
 198
 199/-- Composition of automorphisms is associative (on toFun) -/

used by (9)

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

depends on (12)

Lean names referenced from this declaration's body.