isLocalHomeomorph_iff_isLocalHomeomorphOn_univ

English

A function is a local homeomorph iff it is a local homeomorph on the whole universe.

Русский

Функция является локальным гомеоморфизмом тогда и только тогда, когда она локально гомеоморфна на всём пространстве.

LaTeX

$$$IsLocalHomeomorph f \\iff IsLocalHomeomorphOn f Set.univ$$$

Lean4

theorem isLocalHomeomorph_iff_isLocalHomeomorphOn_univ : IsLocalHomeomorph f ↔ IsLocalHomeomorphOn f Set.univ :=
  ⟨fun h x _ ↦ h x, fun h x ↦ h x trivial⟩

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