comap_discreteTopology — Mathlib

English

If f: X → Y is a local homeomorphism and Y has the discrete topology, then X has the discrete topology.

Русский

Если f: X → Y является локальной гомеоморфией и у Y дискретная топология, то X дискретна.

LaTeX

$$$\\operatorname{IsLocalHomeomorph}(f) \\land [\\operatorname{DiscreteTopology}(Y)] \\Rightarrow \\operatorname{DiscreteTopology}(X)$$$

Lean4

/-- A space that admits a local homeomorphism to a discrete space is itself discrete. -/
theorem comap_discreteTopology (h : IsLocalHomeomorph f) [DiscreteTopology Y] : DiscreteTopology X :=
  (Homeomorph.Set.univ X).discreteTopology_iff.mp h.isLocalHomeomorphOn.discreteTopology_of_image

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