English
Let α be a complete lattice and f: ENNReal → α. Then the supremum over all ENNReal inputs equals the join of the supremum over finite ENNReal inputs and the value at ∞: ⨆ x f(x) = (⨆_{n∈ℝ≥0} f(n)) ⊔ f(∞).
Русский
Пусть α — полная решетка и f: ENNReal → α. Тогда верхняя грань значений f по всем ENNReal равна объединению между верхней гранью по всем конечным ENNReal и значением при ∞: ⨆ x f(x) = (⨆_{t∈ℝ≥0} f(t)) ⊔ f(∞).
LaTeX
$$$$ \bigvee_{x \in \mathbb{R}_{\ge 0}^{\infty}} f(x) = \left( \bigvee_{t \in \mathbb{R}_{\ge 0}} f(t) \right) \sqcup f(\infty). $$$$
Lean4
theorem iSup_ennreal {α : Type*} [CompleteLattice α] {f : ℝ≥0∞ → α} : ⨆ n, f n = (⨆ n : ℝ≥0, f n) ⊔ f ∞ :=
@iInf_ennreal αᵒᵈ _ _
