iUnion_iInter_ge_nat_add — Mathlib

English

For a function f: ℕ → Set α and a natural number n, the union of intersections over i≥n of f(i+k) equals the union of intersections of f(i).

Русский

Для функции f: ℕ → Set α и натурального числа n, объединение пересечений по i≥n f(i+k) равняется объединению пересечений f(i).

LaTeX

$$$\\bigcup_n\\bigcap_{i\\ge n} f(i+k) = \\bigcup_n\\bigcap_{i\\ge n} f(i)$$$

Lean4

@[simp]
theorem iUnion_iInter_ge_nat_add (f : ℕ → Set α) (k : ℕ) : ⋃ n, ⋂ i ≥ n, f (i + k) = ⋃ n, ⋂ i ≥ n, f i :=
  iSup_iInf_ge_nat_add f k

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