t1Space — Mathlib

English

If X is a T1-space, then any Subtype p ⊆ X is also a T1-space.

Русский

Если X — T1-пространство, то подпространство, заданное p ⊆ X, тоже является T1-пространством.

LaTeX

$$$ \text{T1Space } X \Rightarrow \text{T1Space } (\{x:\,X\mid p(x)\})$, i.e., Subtype p is T1-space.$$

Lean4

instance t1Space {X : Type u} [TopologicalSpace X] [T1Space X] {p : X → Prop} : T1Space (Subtype p) :=
  IsEmbedding.subtypeVal.t1Space

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