toHomeomorph_symm — Mathlib

English

For a bijection e between X and Y that induces a homeomorphism, the inverse of the induced homeomorphism is the induced homeomorphism of the inverse bijection.

Русский

Пусть существует биекция e: X → Y, которая порождает гомеоморфизм; тогда обратный гомеоморфизм, полученный из инверсии e, совпадает с соответствующим образом полученным гомеоморфизмом.

LaTeX

$$$ (e^{\\mathrm{toHomeomorph}}(he)).\\mathrm{symm} = e^{\\mathrm{symm}}.toHomeomorph (\\lambda s. by\\ convert (he _).\\mathrm{symm}; \\mathrm{simp}) $$$

Lean4

@[simp]
theorem toHomeomorph_symm (e : X ≃ Y) (he) :
    (e.toHomeomorph he).symm = e.symm.toHomeomorph fun s ↦ by convert (he _).symm; simp :=
  rfl

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