English
If the codomain β is discrete and f: α → β is continuous and injective, then α is discrete.
Русский
Если кодом β дискретная топология и f: α → β непрерывна и инъективна, то α дискретна.
LaTeX
$$$\text{Continuous}(f) \land \text{Injective}(f) \Rightarrow \text{DiscreteTopology}(\alpha)$$$
Lean4
/-- If the codomain of a continuous injective function has discrete topology,
then so does the domain.
See also `Embedding.discreteTopology` for an important special case. -/
theorem of_continuous_injective {β : Type*} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] {f : α → β}
(hc : Continuous f) (hinj : Injective f) : DiscreteTopology α :=
discreteTopology_iff_forall_isOpen.2 fun s ↦ hinj.preimage_image s ▸ (isOpen_discrete _).preimage hc
