English
A space is completely regular iff for every point x and every open neighborhood K of x, there exists a continuous map to the unit interval that vanishes at x and is equal to 1 outside K.
Русский
Пространство полностью регулярное тогда и только тогда, когда для любой точки x и открытого окрещения K существует непрерывная отображение в единичный интервал, равное 0 в x и 1 вне K.
LaTeX
$$$\\text{CompletelyRegularSpace }X \\iff \\forall x\\in X\\, \\forall K\\subseteq X\\ (IsOpen K \\land x \\in K)\\to\\exists f:X\\to I\\ (Continuous f \\land f(x)=0 \\land EqOn f 1 K^c)$$$
Lean4
theorem completelyRegularSpace_iff_isOpen :
CompletelyRegularSpace X ↔
∀ (x : X), ∀ K : Set X, IsOpen K → x ∈ K → ∃ f : X → I, Continuous f ∧ f x = 0 ∧ EqOn f 1 Kᶜ :=
by
conv_lhs =>
tactic =>
simp_rw +singlePass [completelyRegularSpace_iff, compl_surjective.forall, isClosed_compl_iff, mem_compl_iff,
not_not]
