iInf_toSubalgebra — Mathlib

English

Let {S_i} be a family of StarSubalgebras of A over R. Then the subalgebra underlying the infimum equals the infimum of the underlying subalgebras: (⨅ i, S_i).toSubalgebra = ⨅ i, (S_i).toSubalgebra.

Русский

Пусть {S_i} — семейство StarSubalgebra R–A. Тогда подалгебра, лежащая в их инфимумах, равна инфимума каждой из соответствующих подалгебр: (⨅ i, S_i).toSubalgebra = ⨅ i, (S_i).toSubalgebra.

LaTeX

$$$ (\\inf_{i} S_i).toSubalgebra = \\inf_{i} (S_i).toSubalgebra $$$

Lean4

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

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