α : Type u_1
β : Type ?u.121287
γ : Type ?u.121290
ι : Type ?u.121293
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ (⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f (i + k)) = ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f i
α : Type u_1
β : Type ?u.121287
γ : Type ?u.121290
ι : Type ?u.121293
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ liminf (fun i => f (i + k)) atTop = liminf f atTop
simp_rw [liminf_eq_iSup_iInf_of_nat]
no goals
α : Type u_1
β : Type ?u.121287
γ : Type ?u.121290
ι : Type ?u.121293
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ (⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f (i + k)) = ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f i
exact iSup_iInf_ge_nat_add f k