toHomeomorph_of_bijective — Mathlib

English

A bijective local homeomorphism is a homeomorphism.

Русский

Биективный локальный гомеоморфизм — это гомеоморфизм.

LaTeX

$$$\operatorname{IsLocalHomeomorph}(f) \land f \text{ bijective} \Rightarrow f \text{ is a homeomorphism}$$$

Lean4

/-- A bijective local homeomorphism is a homeomorphism. -/
noncomputable def toHomeomorph_of_bijective (hf : IsLocalHomeomorph f) (hb : f.Bijective) : X ≃ₜ Y :=
  (Equiv.ofBijective f hb).toHomeomorphOfContinuousOpen hf.continuous hf.isOpenMap

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