inf_mem_subalgebra_closure — Mathlib

English

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

Русский

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

LaTeX

$$f ⊓ g ∈ A^{topologicalClosure}$$

Lean4

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

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