iUnion_unpair — Mathlib

English

Union over n of f(n.unpair.1, n.unpair.2) equals the double union over i and j of f(i,j).

Русский

Объединение по n от f(n.unpair.1, n.unpair.2) равно двойному объединению по i и j: f(i,j).

LaTeX

$$$ \bigcup_{n \in \mathbb{N}} f(\operatorname{fst}(\operatorname{unpair}(n)), \operatorname{snd}(\operatorname{unpair}(n))) = \bigcup_{i \in \mathbb{N}} \bigcup_{j \in \mathbb{N}} f(i,j). $$$

Lean4

theorem iUnion_unpair {α} (f : ℕ → ℕ → Set α) : ⋃ n : ℕ, f n.unpair.1 n.unpair.2 = ⋃ (i : ℕ) (j : ℕ), f i j :=
  iSup_unpair f

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