separatesPoints_continuous

Stream: Is there code for X?

[Kalle Kytölä]

Do we have that in reasonable spaces continuous real-valued functions separate points?

This is a direct consequence of Urysohn's lemma docs#exists_continuous_zero_one_of_isClosed, but I expected to find this special case conclusion spelled with docs#Set.SeparatesPoints, since that notion exists. I ended up not needing this, but I was wondering if it exists and if it should exist.

import Mathlib.Topology.UrysohnsLemma
import Mathlib.Data.Complex.Abs

open Set

variable {X : Type*} [TopologicalSpace X]

lemma separatesPoints_continuous_of_normalSpace_of_T1Space [NormalSpace X] [T1Space X] :
    SeparatesPoints (Continuous : Set (X → ℝ)) := by
  intro x y x_ne_y
  obtain ⟨f, f_eq_zero, f_eq_one, _⟩ :=
    exists_continuous_zero_one_of_isClosed (isClosed_singleton (x := x)) (isClosed_singleton (x := y))
      (disjoint_singleton.mpr x_ne_y)
  refine ⟨f, f.continuous, by aesop⟩

[Kalle Kytölä]

Interestingly, #minimize_imports told me that importing Mathlib.Topology.UrysohnsLemma was not good enough, and I certainly wanted Mathlib.Data.Complex.Abs, too. :upside_down: I probably did (although removing that second import doesn't break anything...).

[Jireh Loreaux]

I don't think we have any spelling phrased in terms of docs#Set.SeparatesPoints, but I just want to point out that docs#T35Space is enough.

[Kalle Kytölä]

Ok, so:

import Mathlib.Topology.CompletelyRegular

open Set

variable {X : Type*} [TopologicalSpace X]

lemma separatesPoints_continuous_of_T35Space [T35Space X] :
    SeparatesPoints (Continuous : Set (X → ℝ)) := 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
  refine ⟨fun x ↦ f x, continuous_subtype_val.comp f_cont, by aesop⟩

[Kalle Kytölä]

And although I don't need it now, I decided to open PR #11831, since I'd still expect this spelling to be found in the library.

[Matias Heikkilä]

Thank for working on my file @Kalle Kytölä :smile: This actually nudged me to polish some code I hadn't shared.

I would like to prove that docs#stoneCechUnit is a dense embedding for a T35Space X. I have sketched a proof that it's injective (#12536). Feedback welcome :pray:

[Matias Heikkilä]

Let me know if I can in some way help getting some feedback on #12536 :+1:

[Johan Commelin]

Thanks! I left a comment.