completely_regular_isOpen — Mathlib

English

In a completely regular space, for any x and open K containing x, there exists a continuous map to I with the same separation properties.

Русский

В полностью регулярном пространстве для любой точки x и открытого K, содержащего x, существует непрерывное отображение в I, реализующее тот же разделительный характер.

LaTeX

$$$\\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 completely_regular_isOpen [CompletelyRegularSpace X] :
    ∀ (x : X), ∀ K : Set X, IsOpen K → x ∈ K → ∃ f : X → I, Continuous f ∧ f x = 0 ∧ EqOn f 1 Kᶜ :=
  completelyRegularSpace_iff_isOpen.mp inferInstance

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