X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := attachBound ↑f
⊢ abs ↑f ∈ Subalgebra.topologicalClosure A
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
⊢ abs ↑f ∈ Subalgebra.topologicalClosure A
let f' := attachBound (f : C(X, ℝ))
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := attachBound ↑f
abs : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ) := mk fun x => Abs.abs ↑x
⊢ ContinuousMap.abs ↑f ∈ Subalgebra.topologicalClosure A
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := attachBound ↑f
⊢ abs ↑f ∈ Subalgebra.topologicalClosure A
let abs : C(Set.Icc (-‖f‖) ‖f‖, ℝ) := { toFun := fun x : Set.Icc (-‖f‖) ‖f‖ => |(x : ℝ)| }
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := attachBound ↑f
abs : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ) := mk fun x => Abs.abs ↑x
⊢ comp abs f' ∈ Subalgebra.topologicalClosure A
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := attachBound ↑f
abs : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ) := mk fun x => Abs.abs ↑x
⊢ ContinuousMap.abs ↑f ∈ Subalgebra.topologicalClosure A
change abs.comp f' ∈ A.topologicalClosure
no goals
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := attachBound ↑f
abs : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ) := mk fun x => Abs.abs ↑x
⊢ comp abs f' ∈ Subalgebra.topologicalClosure A
apply comp_attachBound_mem_closure