iInter_nat_add — Mathlib

English

If f is antitone as a function ℕ → Set α, then the intersection over all n of f(n+k) equals the intersection over all n of f(n).

Русский

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

LaTeX

$$$\\operatorname{Antitone} f \\Rightarrow (\\bigcap_n f(n+k) = \\bigcap_n f(n))$$$

Lean4

theorem _root_.Antitone.iInter_nat_add {f : ℕ → Set α} (hf : Antitone f) (k : ℕ) : ⋂ n, f (n + k) = ⋂ n, f n :=
  hf.iInf_nat_add k

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