symm — Mathlib

English

The composition of two structomorphisms is a structomorphism.

Русский

Перебор структуроморфизмов является структуроморфизмом.

LaTeX

$$Structomorph.trans$$

Lean4

/-- The inverse of a structomorphism is a structomorphism. -/
def symm (e : Structomorph G M M') : Structomorph G M' M :=
  { e.toHomeomorph.symm with
    mem_groupoid := by
      intro c c' hc hc'
      have : (c'.symm ≫ₕ e.toHomeomorph.toOpenPartialHomeomorph ≫ₕ c).symm ∈ G := G.symm (e.mem_groupoid c' c hc' hc)
      rwa [trans_symm_eq_symm_trans_symm, trans_symm_eq_symm_trans_symm, symm_symm, trans_assoc] at this }

Похожие утверждения