iInter_unpair — Mathlib

English

Intersection over n of f(n.unpair.1, n.unpair.2) equals the double intersection over i,j of f(i,j).

Русский

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

LaTeX

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

Lean4

theorem iInter_unpair {α} (f : ℕ → ℕ → Set α) : ⋂ n : ℕ, f n.unpair.1 n.unpair.2 = ⋂ (i : ℕ) (j : ℕ), f i j :=
  iInf_unpair f

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