coe_sInf — Mathlib

English

The sInf of a set of subalgebras corresponds to the sInf of their NonUnitalSubalgebra images.

Русский

sInf множества подалгебр соответствует sInf их образов в NonUnitalSubalgebra.

LaTeX

$$$sInf S \\;\\text{(as Subalgebra)} = sInf (\\{ S \\text{.toNonUnitalSubalgebra} : S \\in S \\})$$$

Lean4

@[simp, norm_cast]
theorem coe_sInf (S : Set (NonUnitalStarSubalgebra R A)) : (↑(sInf S) : Set A) = ⋂ s ∈ S, ↑s :=
  sInf_image

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