abs_mem_subalgebra_closure — Mathlib

English

The absolute value of a function f ∈ A lies in the topological closure of A when A⊂C(X,ℝ).

Русский

Модуль функции f принадлежит топологическому замыканию A в C(X,ℝ).

LaTeX

$$$|f| \in A^{\mathrm{topologicalClosure}}$$$

Lean4

theorem abs_mem_subalgebra_closure (A : Subalgebra ℝ C(X, ℝ)) (f : A) : |(f : C(X, ℝ))| ∈ A.topologicalClosure :=
  by
  let f' := attachBound (f : C(X, ℝ))
  let abs : C(Set.Icc (-‖f‖) ‖f‖, ℝ) := { toFun := fun x : Set.Icc (-‖f‖) ‖f‖ => |(x : ℝ)| }
  change abs.comp f' ∈ A.topologicalClosure
  apply comp_attachBound_mem_closure

Похожие утверждения