instCompletelyNormalSpaceSubtype — Mathlib

English

If X is completely normal and p defines a subset, then the subspace { x ∈ X | p(x) } is completely normal.

Русский

Если X полностью нормальное, то подпространство { x ∈ X | p(x) } тоже полностью нормальное.

LaTeX

$$[$ \\text{CompletelyNormalSpace}(X) $] {p : X \\to \\Prop} : [\\text{CompletelyNormalSpace}({ x // p x })] $$

Lean4

/-- A subspace of a completely normal space is a completely normal space. -/
instance [CompletelyNormalSpace X] {p : X → Prop} : CompletelyNormalSpace { x // p x } :=
  IsEmbedding.subtypeVal.completelyNormalSpace

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