separatesPoints_continuous_of_t35Space_Icc

English

SeparatesPoints using continuous functions into the unit interval I.

Русский

Разделение точек непрерывными функциями в единичном интервале I.

LaTeX

$$[SeparatesPoints {f:X→I | Continuous f}]$$

Lean4

theorem separatesPoints_continuous_of_t35Space_Icc [T35Space X] : SeparatesPoints {f : X → I | Continuous f} :=
  by
  intro x y x_ne_y
  obtain ⟨f, f_cont, f_zero, f_one⟩ := CompletelyRegularSpace.completely_regular x { y } isClosed_singleton x_ne_y
  exact ⟨f, f_cont, by simp_all⟩

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