coe_starClosure — Mathlib

English

The starClosure of a NonUnitalSubalgebra S is the smallest nonunital subalgebra containing both S and its star, with a witness that star of any element of S is in the closure.

Русский

Звёздочное замыкание nonunitalSubalgebra S — наименьшее ненулевое подполья, содержащее как S, так и star S, с доказательством того, что star любого элемента принадлежит замыканию.

LaTeX

$$$ \mathrm{starClosure}(S) \\text{ is the smallest } NUSA \\text{ with } S, \ star(S) \subseteq NUSA. $$$

Lean4

@[simp]
theorem coe_starClosure (S : NonUnitalSubalgebra R A) :
    (S.starClosure : Set A) = (S ⊔ star S : NonUnitalSubalgebra R A) :=
  rfl

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