isHomeomorph_iff_exists_homeomorph

English

A map is a homeomorphism iff it is the underlying map of a bundled homeomorphism h : X ≃ₜ Y.

Русский

Отображение является гомеоморфизмом тогда и только тогда, когда оно является базовой функцией связанного гомеоморфизма h : X ≃ₜ Y.

LaTeX

$$$\IsHomeomorph(f) \iff \exists h : X \simeq_{\mathrm{Top}} Y, h = f$$$

Lean4

/-- A map is a homeomorphism iff it is the map underlying a bundled homeomorphism `h : X ≃ₜ Y`. -/
theorem isHomeomorph_iff_exists_homeomorph : IsHomeomorph f ↔ ∃ h : X ≃ₜ Y, h = f :=
  ⟨fun hf => ⟨hf.homeomorph f, rfl⟩, fun ⟨h, h'⟩ => h' ▸ h.isHomeomorph⟩

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