t0Space — Mathlib

English

If X is a T0 space, then any subspace defined by a predicate p, i.e. the set {x in X | p x}, with the subspace topology, is also T0.

Русский

Если X — T0-пространство, то любое подпространство, заданное предикатом p, то есть {x ∈ X | p(x)}, с поддополнительной топологией, тоже является T0.

LaTeX

$$$T0Space(\\mathrm{Subtype}(p))$$$

Lean4

@[stacks 0B31 "part 1"]
instance t0Space [T0Space X] {p : X → Prop} : T0Space (Subtype p) :=
  IsEmbedding.subtypeVal.t0Space

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