star_self_mem — Mathlib

English

The star of the generator, i.e., $\\star x$, lies in the elemental subalgebra generated by x.

Русский

Обратное звездное к x принадлежит элементальной подпалгебре, порождаемой x.

LaTeX

$$$\\star x \\in \\operatorname{elemental}_R(x).$$$

Lean4

@[simp, aesop safe (rule_sets := [SetLike])]
theorem star_self_mem (x : A) : star x ∈ elemental R x :=
  le_topologicalClosure _ <| star_self_mem_adjoin_singleton R x

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