le_of_mem — Mathlib

English

If x is in a closed subalgebra s, then the elemental subalgebra generated by x is contained in s.

Русский

Если x принадлежит замкнутой подпалгебре s, то элементальная подпалгебра, порожденная x, ⊆ s.

LaTeX

$$$\\text{If } IsClosed(s)\\text{ and } x\\in s,\\quad \\operatorname{elemental}_R(x) \\le s.$$$

Lean4

theorem le_of_mem {x : A} {s : NonUnitalStarSubalgebra R A} (hs : IsClosed (s : Set A)) (hx : x ∈ s) :
    elemental R x ≤ s :=
  topologicalClosure_minimal _ (adjoin_le <| by simpa using hx) hs

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