X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : { x // x ∈ A }
⊢ 2⁻¹ • (↑f + ↑g + Abs.abs (↑f - ↑g)) ∈ Subalgebra.topologicalClosure A
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : { x // x ∈ A }
⊢ ↑f ⊔ ↑g ∈ Subalgebra.topologicalClosure A
rw [sup_eq]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : { x // x ∈ A }
⊢ Abs.abs (↑f - ↑g) ∈ Subalgebra.topologicalClosure A
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : { x // x ∈ A }
⊢ 2⁻¹ • (↑f + ↑g + Abs.abs (↑f - ↑g)) ∈ Subalgebra.topologicalClosure A
refine'
  A.topologicalClosure.smul_mem
    (A.topologicalClosure.add_mem
      (A.topologicalClosure.add_mem (A.le_topologicalClosure f.property)
        (A.le_topologicalClosure g.property))
      _)
    _
no goals
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : { x // x ∈ A }
⊢ Abs.abs (↑f - ↑g) ∈ Subalgebra.topologicalClosure A
exact_mod_cast abs_mem_subalgebra_closure A _