le_of_mem — Mathlib

English

If S is closed, then any element of the elemental subalgebra generated by a member x of S lies in S.

Русский

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

LaTeX

$$topologicalClosure_minimal (adjoin_le <| Set.singleton_subset_iff.2 hx) hS$$

Lean4

theorem le_of_mem {S : StarSubalgebra R A} (hS : IsClosed (S : Set A)) {x : A} (hx : x ∈ S) : elemental R x ≤ S :=
  topologicalClosure_minimal (adjoin_le <| Set.singleton_subset_iff.2 hx) hS

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