discreteTopology — Mathlib

English

If Y has the discrete topology and f is an embedding, then X has the discrete topology.

Русский

Если Y дискретна и f — вложение, то у X дискретная топология.

LaTeX

$$$[\text{DiscreteTopology } Y] \; (\mathrm{IsEmbedding}(f)) \Rightarrow \mathrm{DiscreteTopology}(X)$$$

Lean4

/-- The topology induced under an inclusion `f : X → Y` from a discrete topological space `Y`
is the discrete topology on `X`.

See also `DiscreteTopology.of_continuous_injective`. -/
theorem discreteTopology [DiscreteTopology Y] (hf : IsEmbedding f) : DiscreteTopology X :=
  .of_continuous_injective hf.continuous hf.injective

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