iInf_toNonUnitalSubalgebra — Mathlib

English

The iInf of a family of subalgebras, when viewed as NonUnitalSubalgebra, equals the iInf of their NonUnitalSubalgebra images.

Русский

iInf семейства подалгебр равен iInf их образов в NonUnitalSubalgebra.

LaTeX

$$$\\iInf_i S_i .toNonUnitalSubalgebra = \\iInf_i (S_i.toNonUnitalSubalgebra)$$$

Lean4

@[simp]
theorem iInf_toNonUnitalSubalgebra {ι : Sort*} (S : ι → NonUnitalStarSubalgebra R A) :
    (⨅ i, S i).toNonUnitalSubalgebra = ⨅ i, (S i).toNonUnitalSubalgebra :=
  SetLike.coe_injective <| by simp

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