iInf_toSubfield — Mathlib

English

The subfield associated to the infimum of a family of intermediate fields equals the infimum of the associated subfields.

Русский

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

LaTeX

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

Lean4

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

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