iSup_ne_top — Mathlib

English

Let α be a complete lattice and f: ENNReal → α. Then the supremum of f over all finite ENNReal inputs (i.e., under the condition x ≠ ∞) equals the supremum over all finite ENNReal inputs x ∈ ℝ≥0.

Русский

Пусть α — полная решетка и f : ENNReal → α. Тогда наивысшая граница значений f(x) по всем конечным элементам ENNReal равна наивысшей границе значений f(x) по всем элементам ℝ≥0.

LaTeX

$$$$ \bigvee_{x \in \mathbb{R}_{\ge 0}^{\infty} \setminus \{\infty\}} f(x) = \bigvee_{x \in \mathbb{R}_{\ge 0}} f(x). $$$$

Lean4

theorem iSup_ne_top [CompleteLattice α] (f : ℝ≥0∞ → α) : ⨆ (x) (_ : x ≠ ∞), f x = ⨆ x : ℝ≥0, f x :=
  @iInf_ne_top αᵒᵈ _ _

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