case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
⊢ ↑(Subalgebra.topologicalClosure A) = ↑⊤
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
⊢ Subalgebra.topologicalClosure A = ⊤
apply SetLike.ext'
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
L : Subalgebra ℝ C(X, ℝ) := Subalgebra.topologicalClosure A
⊢ ↑(Subalgebra.topologicalClosure A) = ↑⊤
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
⊢ ↑(Subalgebra.topologicalClosure A) = ↑⊤
let L := A.topologicalClosure
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
L : Subalgebra ℝ C(X, ℝ) := Subalgebra.topologicalClosure A
n : Set.Nonempty ↑L
⊢ ↑(Subalgebra.topologicalClosure A) = ↑⊤
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
L : Subalgebra ℝ C(X, ℝ) := Subalgebra.topologicalClosure A
⊢ ↑(Subalgebra.topologicalClosure A) = ↑⊤
have n : Set.Nonempty (L : Set C(X, ℝ)) := ⟨(1 : C(X, ℝ)), A.le_topologicalClosure A.one_mem⟩
case h.e'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
L : Subalgebra ℝ C(X, ℝ) := Subalgebra.topologicalClosure A
n : Set.Nonempty ↑L
⊢ ↑(Subalgebra.topologicalClosure A) = closure ↑L
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
L : Subalgebra ℝ C(X, ℝ) := Subalgebra.topologicalClosure A
n : Set.Nonempty ↑L
⊢ ↑(Subalgebra.topologicalClosure A) = ↑⊤
convert
  sublattice_closure_eq_top (L : Set C(X, ℝ)) n
    (fun f fm g gm => inf_mem_closed_subalgebra L A.isClosed_topologicalClosure ⟨f, fm⟩ ⟨g, gm⟩)
    (fun f fm g gm => sup_mem_closed_subalgebra L A.isClosed_topologicalClosure ⟨f, fm⟩ ⟨g, gm⟩)
    (Subalgebra.SeparatesPoints.strongly
      (Subalgebra.separatesPoints_monotone A.le_topologicalClosure w))
no goals
case h.e'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
L : Subalgebra ℝ C(X, ℝ) := Subalgebra.topologicalClosure A
n : Set.Nonempty ↑L
⊢ ↑(Subalgebra.topologicalClosure A) = closure ↑L
simp