iSup_toSubfield — Mathlib

English

The subfield associated to the supremum (join) of a family of intermediate fields equals the supremum of the associated subfields.

Русский

Подполе, соответствующее верхней границе (объединению) семейства промежуточных полей, равно верхней границе подпольев.

LaTeX

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

Lean4

@[simp]
theorem iSup_toSubfield {ι : Sort*} [Nonempty ι] (S : ι → IntermediateField F E) :
    (iSup S).toSubfield = ⨆ i, (S i).toSubfield := by
  simp only [iSup, Set.range_nonempty, sSup_toSubfield, ← Set.range_comp, Function.comp_def]

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