English
If s ⊆ Y is discrete and f:X→Y is continuous and injective, then the preimage f^{-1}(s) is discrete in X.
Русский
Если s ⊆ Y дискретно, а f:X→Y непрерывно и инъективно, то предобраз f^{-1}(s) дискретно в X.
LaTeX
$$$\\forall X,Y,\\; [\\text{TopologicalSpace } X], [\\text{TopologicalSpace } Y],\\; s\\subseteq Y,\\; [\\text{DiscreteTopology } s],\\; f:X\\to Y,\\; (\\text{Continuous}(f) \\wedge \\text{Injective}(f)) \\Rightarrow \\text{DiscreteTopology}(f^{-1}(s)).$$$
Lean4
/-- Let `s` be a discrete subset of a topological space. Then the preimage of `s` by
a continuous injective map is also discrete. -/
theorem preimage_of_continuous_injective {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] (s : Set Y)
[DiscreteTopology s] {f : X → Y} (hc : Continuous f) (hinj : Function.Injective f) : DiscreteTopology (f ⁻¹' s) :=
DiscreteTopology.of_continuous_injective (β := s) (Continuous.restrict (by exact fun _ x ↦ x) hc)
((MapsTo.restrict_inj _).mpr hinj.injOn)
