pith. machine review for the scientific record. sign in
theorem proved term proof

compAutomorphism_inv_left_toFun

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)

 222theorem compAutomorphism_inv_left_toFun (T : RecognitionAutomorphism r) (c : C) :
 223    (compAutomorphism T.inv T).toFun c = c := by

proof body

Term-mode proof.

 224  simp only [compAutomorphism, RecognitionAutomorphism.inv, Function.comp_apply]
 225  exact T.left_inv c
 226
 227/-- The composition T ∘ T⁻¹ acts as identity -/

used by (1)

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

depends on (10)

Lean names referenced from this declaration's body.