separatesPoints_continuous_of_t35Space

English

In a CR space, the family of continuous real-valued functions separates points.

Русский

В CR-пространстве множество непрерывных функций в реальных значениях разделяет точки.

LaTeX

$$$[SeparatesPoints \\{f:X\\to \\mathbb{R} \\mid Continuous f\\}]$$$

Lean4

theorem separatesPoints_continuous_of_t35Space [T35Space X] : SeparatesPoints {f : X → ℝ | 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 ⟨fun x ↦ f x, continuous_subtype_val.comp f_cont, by simp_all⟩

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