coe_iInf — Mathlib

English

The set underlying the infimum over a family indexed by i is the intersection over i of the corresponding interval carriers.

Русский

Множество, соответствующее инфимууму по индексу i, есть пересечение по i соответствующих множеств интервалов.

LaTeX

$$$$ ↑(\\bigsqcap_i f(i)) = \\bigcap_i (f(i) : Set \\alpha). $$$$

Lean4

@[simp, norm_cast]
theorem coe_iInf [DecidableLE α] (f : ι → Interval α) : ↑(⨅ i, f i) = ⋂ i, (f i : Set α) := by simp [iInf]

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