discreteTopology_range_iff — Mathlib

English

If f is a local homeomorphism, then the discrete topology on Set.range f is equivalent to the discrete topology on X.

Русский

Если f — локальная гомеоморфия, то дискретная топология на Set.range f эквивалентна дискретной топологии X.

LaTeX

$$$\operatorname{DiscreteTopology}(\operatorname{Set.range} f) \iff \operatorname{DiscreteTopology}(X)\quad\text{assuming } \operatorname{IsLocalHomeomorph}(f)$$$

Lean4

theorem discreteTopology_range_iff (h : IsLocalHomeomorph f) : DiscreteTopology (Set.range f) ↔ DiscreteTopology X :=
  by
  rw [← Set.image_univ, ← (Homeomorph.Set.univ X).discreteTopology_iff]
  exact h.isLocalHomeomorphOn.discreteTopology_image_iff isOpen_univ

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