α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f✝ : α → β
x✝ y : α
r : ℝ
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist ((f^[n]) x) ((f^[n] ∘ f) x) ≤ ↑K ^ n * dist x (f x)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f✝ : α → β
x✝ y : α
r : ℝ
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist ((f^[n]) x) ((f^[n + 1]) x) ≤ dist x (f x) * ↑K ^ n
rw [iterate_succ, mul_comm]
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f✝ : α → β
x✝ y : α
r : ℝ
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist ((f^[n]) x) ((f^[n] ∘ f) x) ≤ ↑K ^ n * dist x (f x)
simpa only [NNReal.coe_pow] using (hf.iterate n).dist_le_mul x (f x)