sup_mem_subalgebra_closure — Mathlib

English

The supremum of two maps f and g in a subalgebra A of C(X,ℝ) lies in the topological closure of A.

Русский

supremum двух отображений принадлежит замыканию подалгебры.

LaTeX

$$f \sqcup g ∈ A^{topologicalClosure}$$

Lean4

theorem sup_mem_subalgebra_closure (A : Subalgebra ℝ C(X, ℝ)) (f g : A) :
    (f : C(X, ℝ)) ⊔ (g : C(X, ℝ)) ∈ A.topologicalClosure :=
  by
  rw [sup_eq_half_smul_add_add_abs_sub' ℝ]
  refine
    A.topologicalClosure.smul_mem
      (A.topologicalClosure.add_mem
        (A.topologicalClosure.add_mem (A.le_topologicalClosure f.property) (A.le_topologicalClosure g.property)) ?_)
      _
  exact mod_cast abs_mem_subalgebra_closure A _

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