coe_iInf — Mathlib

English

For a family S: ι → Subfield K, the carrier of the infimum ⨅ i, S i equals the intersection over i of S i: (↑(⨅ i, S i) : Set K) = ⋂ i, S i.

Русский

Для семейства подполья S i носитель наибольшего нижнего предела ⨅ i, S i равен пересечению всех S i: (↑(⨅ i, S i) : Set K) = ⋂ i, S i.

LaTeX

$$$(\uparrow(⨅ i, S i) : Set K) = \bigcap i, (S i)$$$

Lean4

@[simp, norm_cast]
theorem coe_iInf {ι : Sort*} {S : ι → Subfield K} : (↑(⨅ i, S i) : Set K) = ⋂ i, S i := by
  simp only [iInf, coe_sInf, Set.biInter_range]

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