le_of_mem — Mathlib

English

Let S be a closed Subalgebra of A and let x be an element of S. Then the elemental subalgebra of A generated by x over R is contained in S; i.e., elemental R x ≤ S.

Русский

Пусть S — замкнутая подалгебра A и x ∈ S. Тогда элементарная подалгебра R x, порождаемая x над R, содержится в S; то есть elemental R x ≤ S.

LaTeX

$$$R$ — коммутативная полейная полуалгебра; $A$ — топологическая $R$-алгебра; $s\le A$ — замкнутая подалгебра; $x\in s$. Тогда $\operatorname{elemental}_R(x) \le s$.$$

Lean4

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

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