star_self_mem_adjoin_singleton — Mathlib

English

Let A be a star-ordered algebra over R, and let x be an element of A. Then the star of x, denoted x*, lies in the smallest star-subalgebra of A containing R and x; i.e., x* ∈ adjoin_R({x}).

Русский

Пусть A — звёздная алгебра над R, и возьмём элемент x ∈ A. Тогда звезда x, обозначаемая x*, принадлежит наименьшей звёздной подпалебре, порождаемой R и x; то есть x* ∈ adjoin_R({x}).

LaTeX

$$$ \star x \in \operatorname{adjoin}_R(\{x\}) $$$

Lean4

theorem star_self_mem_adjoin_singleton (x : A) : star x ∈ adjoin R ({ x } : Set A) :=
  star_mem <| self_mem_adjoin_singleton R x

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