α : Type u_1
β : Type ?u.123164
γ : Type ?u.123167
ι : Type ?u.123170
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ (⨅ (i : ℕ), ↑f (⨆ (i_1 : ℕ), (↑f^[i_1 + i]) a)) = ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f^[i + n]) a
α : Type u_1
β : Type ?u.123164
γ : Type ?u.123167
ι : Type ?u.123170
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ↑f (limsup (fun n => (↑f^[n]) a) atTop) = limsup (fun n => (↑f^[n]) a) atTop
rw [limsup_eq_iInf_iSup_of_nat', map_iInf]
α : Type u_1
β : Type ?u.123164
γ : Type ?u.123167
ι : Type ?u.123170
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (↑f^[i_1 + Nat.succ i]) a) = ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f^[i + n]) a
α : Type u_1
β : Type ?u.123164
γ : Type ?u.123167
ι : Type ?u.123170
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ (⨅ (i : ℕ), ↑f (⨆ (i_1 : ℕ), (↑f^[i_1 + i]) a)) = ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f^[i + n]) a
simp_rw [_root_.map_iSup, ← Function.comp_apply (f := f), ← Function.iterate_succ' f,
  ← Nat.add_succ]
α : Type u_1
β : Type ?u.123164
γ : Type ?u.123167
ι : Type ?u.123170
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (↑f^[i_1 + Nat.succ i]) a) ≤ ⨆ (i : ℕ), (↑f^[i]) a
α : Type u_1
β : Type ?u.123164
γ : Type ?u.123167
ι : Type ?u.123170
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (↑f^[i_1 + Nat.succ i]) a) =
    (⨅ (i : ℕ) (_ : (fun x x_1 => x < x_1) 0 i), ⨆ (i_1 : ℕ), (↑f^[i_1 + i]) a) ⊓
      ⨅ (i : ℕ) (_ : ¬(fun x x_1 => x < x_1) 0 i), ⨆ (i_1 : ℕ), (↑f^[i_1 + i]) a
simp only [not_lt, le_zero_iff, iInf_iInf_eq_left, add_zero, iInf_nat_gt_zero_eq, left_eq_inf]
α : Type u_1
β : Type ?u.123164
γ : Type ?u.123167
ι : Type ?u.123170
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ (⨆ (j : ℕ), (↑f^[j + (0 + 1)]) a) ≤ ⨆ (i : ℕ), (↑f^[i]) a
α : Type u_1
β : Type ?u.123164
γ : Type ?u.123167
ι : Type ?u.123170
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (↑f^[i_1 + Nat.succ i]) a) ≤ ⨆ (i : ℕ), (↑f^[i]) a
refine' (iInf_le (fun i => ⨆ j, (f^[j + (i + 1)]) a) 0).trans _
α : Type u_1
β : Type ?u.123164
γ : Type ?u.123167
ι : Type ?u.123170
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ∀ (i : ℕ), (↑f^[i + 1]) a ≤ ⨆ (i : ℕ), (↑f^[i]) a
α : Type u_1
β : Type ?u.123164
γ : Type ?u.123167
ι : Type ?u.123170
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ (⨆ (j : ℕ), (↑f^[j + (0 + 1)]) a) ≤ ⨆ (i : ℕ), (↑f^[i]) a
simp only [zero_add, Function.comp_apply, iSup_le_iff]
no goals
α : Type u_1
β : Type ?u.123164
γ : Type ?u.123167
ι : Type ?u.123170
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ∀ (i : ℕ), (↑f^[i + 1]) a ≤ ⨆ (i : ℕ), (↑f^[i]) a
exact fun i => le_iSup (fun i => (f^[i]) a) (i + 1)