English
Let X be a compact topological space and L a nonempty lattice of real-valued continuous functions on X such that L is closed under pointwise infimum and supremum and separates points strongly. Then the uniform closure of L is all of C(X, R); i.e., L is dense in C(X, R).
Русский
Пусть X — компактное топологическое пространство, L — непустая подмножество из C(X, R), замкнутое относительно поэлементной операцией встречной и объединения, образующее решетку функций, и такое, что L сильно разделяет точки. Тогда плотность L в C(X, R) по норме униформной близости: closure(L) = C(X, R).
LaTeX
$$$\overline{L} = C(X, \mathbb{R}).$$$
Lean4
theorem sublattice_closure_eq_top (L : Set C(X, ℝ)) (nA : L.Nonempty) (inf_mem : ∀ᵉ (f ∈ L) (g ∈ L), f ⊓ g ∈ L)
(sup_mem : ∀ᵉ (f ∈ L) (g ∈ L), f ⊔ g ∈ L) (sep : L.SeparatesPointsStrongly) : closure L = ⊤ := by
-- We start by boiling down to a statement about close approximation.
rw [eq_top_iff]
rintro f -
refine Filter.Frequently.mem_closure ((Filter.HasBasis.frequently_iff Metric.nhds_basis_ball).mpr fun ε pos => ?_)
simp only [Metric.mem_ball]
-- It will be helpful to assume `X` is nonempty later,
-- so we get that out of the way here.
by_cases nX : Nonempty X
swap
·
exact
⟨nA.some, (dist_lt_iff pos).mpr fun x => False.elim (nX ⟨x⟩), nA.choose_spec⟩
/-
The strategy now is to pick a family of continuous functions `g x y` in `A`
with the property that `g x y x = f x` and `g x y y = f y`
(this is immediate from `h : SeparatesPointsStrongly`)
then use continuity to see that `g x y` is close to `f` near both `x` and `y`,
and finally using compactness to produce the desired function `h`
as a maximum over finitely many `x` of a minimum over finitely many `y` of the `g x y`.
-/
dsimp only [Set.SeparatesPointsStrongly] at sep
choose g hg w₁ w₂ using sep f
let U : X → X → Set X := fun x y => {z | f z - ε < g x y z}
have U_nhds_y : ∀ x y, U x y ∈ 𝓝 y := by
intro x y
refine IsOpen.mem_nhds ?_ ?_
· apply isOpen_lt <;> fun_prop
· rw [Set.mem_setOf_eq, w₂]
exact sub_lt_self _ pos
let ys : X → Finset X := fun x => (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x)).choose
let ys_w : ∀ x, ⋃ y ∈ ys x, U x y = ⊤ := fun x => (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x)).choose_spec
have ys_nonempty : ∀ x, (ys x).Nonempty := fun x =>
Set.nonempty_of_union_eq_top_of_nonempty _ _ nX
(ys_w x)
-- Thus for each `x` we have the desired `h x : A` so `f z - ε < h x z` everywhere
-- and `h x x = f x`.
let h : X → L := fun x =>
⟨(ys x).sup' (ys_nonempty x) fun y => (g x y : C(X, ℝ)), Finset.sup'_mem _ sup_mem _ _ _ fun y _ => hg x y⟩
have lt_h : ∀ x z, f z - ε < (h x : X → ℝ) z := by
intro x z
obtain ⟨y, ym, zm⟩ := Set.exists_set_mem_of_union_eq_top _ _ (ys_w x) z
dsimp [h]
simp only [coe_sup', Finset.sup'_apply, Finset.lt_sup'_iff]
exact ⟨y, ym, zm⟩
have h_eq : ∀ x, (h x : X → ℝ) x = f x := by intro x;
simp [h, w₁]
-- For each `x`, we define `W x` to be `{z | h x z < f z + ε}`,
let W : X → Set X := fun x =>
{z | (h x : X → ℝ) z < f z + ε}
-- This is still a neighbourhood of `x`.
have W_nhds : ∀ x, W x ∈ 𝓝 x := by
intro x
refine IsOpen.mem_nhds ?_ ?_
· apply isOpen_lt <;> fun_prop
· dsimp only [W, Set.mem_setOf_eq]
rw [h_eq]
exact lt_add_of_pos_right _ pos
let xs : Finset X := (CompactSpace.elim_nhds_subcover W W_nhds).choose
let xs_w : ⋃ x ∈ xs, W x = ⊤ := (CompactSpace.elim_nhds_subcover W W_nhds).choose_spec
have xs_nonempty : xs.Nonempty := Set.nonempty_of_union_eq_top_of_nonempty _ _ nX xs_w
let k : (L : Type _) :=
⟨xs.inf' xs_nonempty fun x => (h x : C(X, ℝ)), Finset.inf'_mem _ inf_mem _ _ _ fun x _ => (h x).2⟩
refine
⟨k.1, ?_, k.2⟩
-- We just need to verify the bound, which we do pointwise.
rw [dist_lt_iff pos]
intro z
rw [show ∀ a b ε : ℝ, dist a b < ε ↔ a < b + ε ∧ b - ε < a by intros;
simp only [← Metric.mem_ball, Real.ball_eq_Ioo, Set.mem_Ioo, and_comm]]
fconstructor
· dsimp
simp only [k, Finset.inf'_lt_iff, ContinuousMap.inf'_apply]
exact Set.exists_set_mem_of_union_eq_top _ _ xs_w z
· dsimp
simp only [k, Finset.lt_inf'_iff, ContinuousMap.inf'_apply]
rintro x -
apply lt_h
