Urysohn's lemma to Stone-Weierstrass theorem

TheoremUrysohn's lemma #

Urysohn's lemma: if s and t are two disjoint closed sets in a normal topological space X, then there exists a continuous function f : X → ℝ such that

f equals zero on s;
f equals one on t;
0 ≤ f x ≤ 1 for all x.

exists_continuous_zero_one_of_isClosed.{u_1} {X : Type u_1} [TopologicalSpace X] [NormalSpace X]
  {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
  ∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1

Sources

Mathlibexists_continuous_zero_one_of_isClosed

Uses 17 · Used by 5

Statement usesBornology · Continuous function · Order

Proof usesAffine function · Characteristic zero · Closure · Euclidean affine space · Field \(\R\) of real numbers · Hausdorff space · Invertible elements · Metric structure · Normed vector space over a normed field · Order topology · Ordered ring · The Triangle Inequality · Topological module · Topological ring

Used byFourier Series · Riemann-Lebesgue lemma (Analysis) · Prokhorov's theorem · Metrization theorems · Tietze extension theorem

TheoremStone-Weierstrass theorem #

The Stone-Weierstrass Approximation Theorem, that a subalgebra A of C(X, ℝ), where X is a compact topological space, is dense if it separates points.

ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints.{u_1} {X : Type u_1}
  [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (w : A.SeparatesPoints) :
  A.topologicalClosure = ⊤