English
Let α be a complete lattice and f: ENNReal → α. Then the infimum of f over all ENNReal inputs equals the infimum over finite ENNReal inputs intersected with the value at ∞: ⨅_{n∈ℕ} f(n) = (⨅_{t∈ℝ≥0} f(t)) ⊓ f(∞).
Русский
Пусть α — полная решетка и f: ENNReal → α. Тогда наименьшая нижняя граница значений f по всем ENNReal ввозможна равна пересечению между наименьшей нижней границей по всем конечным ENNReal и значением в ∞: ⨅_{n∈ℕ} f(n) = (⨅_{t∈ℝ≥0} f(t)) ⊓ f(∞).
LaTeX
$$$$ \bigwedge_{n \in \mathbb{N}} f(n) = \left( \bigwedge_{t \in \mathbb{R}_{\ge 0}} f(t) \right) \wedge f(\infty). $$$$
Lean4
theorem iInf_ennreal {α : Type*} [CompleteLattice α] {f : ℝ≥0∞ → α} : ⨅ n, f n = (⨅ n : ℝ≥0, f n) ⊓ f ∞ :=
(iInf_option f).trans (inf_comm _ _)
