inf_mem_closed_subalgebra — Mathlib

English

If A is closed, the infimum f ⊓ g of any two elements f, g ∈ A actually lies in A (not only in its closure).

Русский

Если A замкнута, то наименьшее между двумя элементами лежит в A.

LaTeX

$$$f \inf g ∈ A$$$

Lean4

theorem inf_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 inf_mem_subalgebra_closure A f g
  apply SetLike.ext'
  symm
  rw [Subalgebra.topologicalClosure_coe, closure_eq_iff_isClosed]
  exact h

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