iInf_toSubalgebra — Mathlib

English

The subalgebra associated to the infimum of a family of intermediate fields equals the infimum of the associated subalgebras.

Русский

Подалгебра, соответствующая инфимуму семейства промежуточных полей, равна инфимума соответствующих подпалгебр.

LaTeX

$$$ (iInf S).toSubalgebra = iInf (\\, i \\mapsto (S i).toSubalgebra \\,)$$$

Lean4

@[simp]
theorem iInf_toSubalgebra {ι : Sort*} (S : ι → IntermediateField F E) :
    (iInf S).toSubalgebra = ⨅ i, (S i).toSubalgebra :=
  SetLike.coe_injective <| by simp [iInf]

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