le_iff_mem — Mathlib

English

Let A be a topological star-algebra over R and let s be a closed subalgebra of A. For any x ∈ A, the elemental subalgebra generated by x, denoted elemental R x, is contained in s if and only if x ∈ s.

Русский

Пусть A — топологическая звёздная алгебра над R и s — замкнутая подалгебра A. Тогда для любого x ∈ A элементарная подалгебра, порожденная x, принадлежит s тогда и только тогда, когда x ∈ s.

LaTeX

$$$\displaystyle \forall x\in A\,\forall s\text{ a StarSubalgebra of }A\text{ with }IsClosed(s),\; (elemental(R,x) \le s) \iff (x \in s) $$$

Lean4

theorem le_iff_mem {x : A} {s : StarSubalgebra R A} (hs : IsClosed (s : Set A)) : elemental R x ≤ s ↔ x ∈ s :=
  ⟨fun h ↦ h (self_mem R x), fun h ↦ le_of_mem hs h⟩

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