English
For a sequence f: ℕ → α and k ∈ ℕ, the expression iSup_i of iInf of iInf with f(i+k) equals iSup_i of iInf over i of f(i) (duality with Nat-add).
Русский
Для последовательности f: ℕ → α и k ∈ ℕ выражение iSup_iInf ... с f(i+k) равно iSup_iInf ... f(i) (дуалитет с Nat-добавлением).
LaTeX
$$$\displaystyle \text{(dual statement)}$$$
Lean4
theorem iSup_iInf_ge_nat_add (f : ℕ → α) (k : ℕ) : ⨆ n, ⨅ i ≥ n, f (i + k) = ⨆ n, ⨅ i ≥ n, f i :=
by
have hf : Monotone fun n => ⨅ i ≥ n, f i := fun n m h => biInf_mono fun i => h.trans
rw [← Monotone.iSup_nat_add hf k]
·
simp_rw [iInf_ge_eq_iInf_nat_add, ← Nat.add_assoc]
-- Not `@[simp]` since the subterm `?f (i + ?k)` produces an ugly higher-order unification problem.
-- (Although the `simpNF` linter does not complain.)
-- See: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/complete_lattice.20and.20has_sup/near/316497982
