coe_iInf — Mathlib

English

For a family of intermediate fields indexed by ι, the underlying set of their indexed infimum equals the intersection of the corresponding sets.

Русский

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

LaTeX

$$$ (\\uparrow (iInf S) : \\mathrm{Set} E) = \\bigcap_i (S_i : \\mathrm{Set} E) $$$

Lean4

@[simp, norm_cast]
theorem coe_iInf {ι : Sort*} (S : ι → IntermediateField F E) : (↑(iInf S) : Set E) = ⋂ i, S i := by simp [iInf]

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