English
If s is a discrete subset of a topological space X and t ⊆ s, then t carries the discrete topology as a subset of X.
Русский
Если s — дискретное подмножество пространства X, и t ⊆ s, то и t наследует дискретную топологию как подмножество X.
LaTeX
$$$\\forall X\\, [\\text{TopologicalSpace } X],\\; s,t\\subseteq X,\\; (\\text{DiscreteTopology } s)\\Rightarrow (t\\subseteq s)\\Rightarrow \\text{DiscreteTopology } t.$$$
Lean4
/-- Let `s, t ⊆ X` be two subsets of a topological space `X`. If `t ⊆ s` and the topology induced
by `X`on `s` is discrete, then also the topology induces on `t` is discrete. -/
theorem of_subset {X : Type*} [TopologicalSpace X] {s t : Set X} (_ : DiscreteTopology s) (ts : t ⊆ s) :
DiscreteTopology t :=
(IsEmbedding.inclusion ts).discreteTopology
