mem_bot — Mathlib

English

For any x ∈ A, x lies in the bottom StarSubalgebra iff x lies in the image of algebra map R → A.

Русский

Для любого x ∈ A верно: x принадлежит нижней StarSubalgebra тогда и только тогда, когда x лежит в образе алгебраического отображения R → A.

LaTeX

$$$ x \\in (\\bot : StarSubalgebra\\; R\\; A) \\;\\Longleftrightarrow\\; x \\in \\operatorname{range}(\\mathrm{algebraMap}\\; R\\; A) $$$

Lean4

theorem mem_bot {x : A} : x ∈ (⊥ : StarSubalgebra R A) ↔ x ∈ Set.range (algebraMap R A) :=
  Iff.rfl

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