English
For a function f: N×N → α into a complete lattice α, the supremum over n of f(n.unpair.1, n.unpair.2) equals the supremum over all i,j of f(i,j).
Русский
Для функции f: N×N → α в Complete lattice α верхняя грань по n от f(n.unpair.1, n.unpair.2) совпадает с верхней гранью по всем i,j: f(i,j).
LaTeX
$$$ \sup_{n \in \mathbb{N}} f(\operatorname{fst}(\operatorname{unpair}(n)), \operatorname{snd}(\operatorname{unpair}(n))) = \sup_{i\in\mathbb{N}, j\in\mathbb{N}} f(i,j). $$$
Lean4
theorem iSup_unpair {α} [CompleteLattice α] (f : ℕ → ℕ → α) :
⨆ n : ℕ, f n.unpair.1 n.unpair.2 = ⨆ (i : ℕ) (j : ℕ), f i j := by
rw [← (iSup_prod : ⨆ i : ℕ × ℕ, f i.1 i.2 = _), ← Nat.surjective_unpair.iSup_comp]
