English
If a closed set s in a separable space has a discrete topology and cardinality at least continuum, then the ambient space is not normal.
Русский
Если закрытое множество s в разделяемом пространстве имеет дискретную топологию и кардинал как минимум континуум, то окружающее пространство не нормальное.
LaTeX
$$$\\text{If } s \\text{ is closed and discrete in a separable normal space, with } |s| \\ge \\mathfrak{c}, \\text{ then the ambient space is not normal.}$$$
Lean4
/-- Let `s` be a closed set in a separable space. If the induced topology on `s` is discrete and `s`
has cardinality at least continuum, then the ambient space is not a normal space. -/
theorem not_normal_of_continuum_le_mk {s : Set X} (hs : IsClosed s) [DiscreteTopology s] (hmk : 𝔠 ≤ #s) :
¬NormalSpace X := fun _ ↦ hs.mk_lt_continuum.not_ge hmk
