case h.e'_5.h.e'_3
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ fixedPoint f hf = efixedPoint f hf x (_ : edist x (f x) ≠ ⊤)
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ Tendsto (fun n => (f^[n]) x) atTop (𝓝 (fixedPoint f hf))
convert tendsto_iterate_efixedPoint hf (edist_ne_top x _)
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ IsFixedPt f (efixedPoint f hf x (_ : edist x (f x) ≠ ⊤))
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ fixedPoint f hf = efixedPoint f hf x (_ : edist x (f x) ≠ ⊤)
refine' (fixedPoint_unique _ _).symm
no goals
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ IsFixedPt f (efixedPoint f hf x (_ : edist x (f x) ≠ ⊤))
apply efixedPoint_isFixedPt