sup_mem_closed_subalgebra — Mathlib

English

If A is closed, then the supremum f ⊔ g of any two elements f,g ∈ A actually lies in A.

Русский

Если A замкнута, то максимум двух функций из A принадлежит A.

LaTeX

$$$f \sqcup g ∈ A$$$

Lean4

theorem sup_mem_closed_subalgebra (A : Subalgebra ℝ C(X, ℝ)) (h : IsClosed (A : Set C(X, ℝ))) (f g : A) :
    (f : C(X, ℝ)) ⊔ (g : C(X, ℝ)) ∈ A :=
  by
  convert sup_mem_subalgebra_closure A f g
  apply SetLike.ext'
  symm
  dsimp
  rw [closure_eq_iff_isClosed]
  exact h

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