iInter_ge_eq_iInter_nat_add — Mathlib

English

For a family of sets u: ℕ → Set α and natural number n, the iterated intersection over i ≥ n of u(i) equals the iterated intersection over i of u(i+n).

Русский

Для семейства множеств u: ℕ → Set α и натурального числа n логическое пересечение по i ≥ n совпадает с пересечением по i от u(i+n).

LaTeX

$$$\\bigcup$ and intersections omitted;\\; \\text{Eq } (\\bigcap_{i \\ge n} u(i)) = \\bigcap_i u(i+n)$$$

Lean4

theorem iInter_ge_eq_iInter_nat_add (u : ℕ → Set α) (n : ℕ) : ⋂ i ≥ n, u i = ⋂ i, u (i + n) :=
  iInf_ge_eq_iInf_nat_add u n

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