case h.e'_4.h.e'_5
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
⊢ edist x (f x) = edist x (f x) * ↑K ^ 0
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
⊢ edist x (efixedPoint f hf x hx) ≤ edist x (f x) / (1 - ↑K)
convert hf.apriori_edist_iterate_efixedPoint_le hx 0
no goals
case h.e'_4.h.e'_5
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
⊢ edist x (f x) = edist x (f x) * ↑K ^ 0
simp only [pow_zero, mul_one]