α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist ((f^[n]) x) (fixedPoint f hf) ≤ dist ((f^[n]) x) ((f ∘ f^[n]) x) / (1 - ↑K)
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist ((f^[n]) x) (fixedPoint f hf) ≤ dist ((f^[n]) x) ((f^[n + 1]) x) / (1 - ↑K)
rw [iterate_succ']
no goals
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist ((f^[n]) x) (fixedPoint f hf) ≤ dist ((f^[n]) x) ((f ∘ f^[n]) x) / (1 - ↑K)
apply hf.dist_fixedPoint_le