mem_starClosure — Mathlib

English

For any S, x ∈ S.starClosure if and only if x ∈ S ⊔ star S. In words, membership in the star-closure coincides with membership in the join of S and its star.

Русский

Для любой подалгебры S и элемента x: x ∈ S^{star-closure} тогда и только тогда, когда x ∈ (S ⊔ S^{*}).

LaTeX

$$$x \in S^{\star-closure} \iff x \in S \lor x \in S^{*} \quad(= x \in S \sqcup S^{*}).$$$

Lean4

@[simp]
theorem mem_starClosure (S : Subalgebra R A) {x : A} : x ∈ S.starClosure ↔ x ∈ S ⊔ star S :=
  Iff.rfl

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