iUnion_nat_add — Mathlib

English

If f is monotone as a function ℕ → Set α, then the union over all n of f(n+k) equals the union over all n of f(n) for any fixed k.

Русский

Если f является монотонной функцией, то объединение по n сдвинутого на k набора f(n+k) совпадает с объединением по всем n f(n).

LaTeX

$$$\\operatorname{Monotone} f \\Rightarrow (\\bigcup_n f(n+k) = \\bigcup_n f(n))$$$

Lean4

theorem _root_.Monotone.iUnion_nat_add {f : ℕ → Set α} (hf : Monotone f) (k : ℕ) : ⋃ n, f (n + k) = ⋃ n, f n :=
  hf.iSup_nat_add k

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