exists_eq_iSup₂_of_lt_top — Mathlib

English

The supremum over natural numbers cast to ENat is the top element: ⨆ n:ℕ, (n : ℕ∞) = ⊤.

Русский

Супремум по натуральным числам, приводимым к ENat, равен вершине: ⨆ n:ℕ, (n : ℕ∞) = ⊤.

LaTeX

$$$\displaystyle \bigl(\bigvee_{n \in \mathbb{N}} (n : \mathbb{N}_\infty)\bigr) = \top$$$

Lean4

theorem exists_eq_iSup₂_of_lt_top {ι₁ ι₂ : Type*} {f : ι₁ → ι₂ → ℕ∞} [Nonempty ι₁] [Nonempty ι₂]
    (h : ⨆ i, ⨆ j, f i j < ⊤) : ∃ i j, f i j = ⨆ i, ⨆ j, f i j :=
  by
  rw [iSup_prod'] at h ⊢
  exact Prod.exists'.mp (exists_eq_iSup_of_lt_top h)

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