case h.e'_5
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : { x // x ∈ A }
⊢ A = Subalgebra.topologicalClosure A
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : { x // x ∈ A }
⊢ ↑f ⊓ ↑g ∈ A
convert inf_mem_subalgebra_closure A f g
case h.e'_5.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : { x // x ∈ A }
⊢ ↑A = ↑(Subalgebra.topologicalClosure A)
case h.e'_5
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : { x // x ∈ A }
⊢ A = Subalgebra.topologicalClosure A
apply SetLike.ext'
case h.e'_5.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : { x // x ∈ A }
⊢ ↑(Subalgebra.topologicalClosure A) = ↑A
case h.e'_5.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : { x // x ∈ A }
⊢ ↑A = ↑(Subalgebra.topologicalClosure A)
symm
case h.e'_5.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : { x // x ∈ A }
⊢ IsClosed ↑A
case h.e'_5.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : { x // x ∈ A }
⊢ ↑(Subalgebra.topologicalClosure A) = ↑A
erw [closure_eq_iff_isClosed]
no goals
case h.e'_5.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : { x // x ∈ A }
⊢ IsClosed ↑A
exact h