toHomeomorph_refl — Mathlib

English

Let X be a topological space. The homeomorphism induced by the identity equivalence on X is the identity homeomorphism on X.

Русский

Пусть X — топологическое пространство. Гомеоморфизм, получаемый из тождественного эквивижа X, является тождественным гомеоморфизмом на X.

LaTeX

$$$ (\\mathrm{Equiv.refl}\\ X).toHomeomorph (\\lambda s. \\mathrm{Iff.rfl}) = \\mathrm{Homeomorph.refl}\\ X $$$

Lean4

@[simp]
theorem toHomeomorph_refl : (Equiv.refl X).toHomeomorph (fun _s ↦ Iff.rfl) = Homeomorph.refl _ :=
  rfl

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