Hofer's lemma
This is an elementary lemma about complete metric spaces. It is motivated by an application to the bubbling-off analysis for holomorphic curves in symplectic topology. We are very far away from having these applications, but the proof here is a nice example of a proof needing to construct a sequence by induction in the middle of the proof.
References:
- H. Hofer and C. Viterbo, The Weinstein conjecture in the presence of holomorphic spheres
theorem
hofer
{X : Type u_1}
[metric_space X]
[complete_space X]
(x : X)
(ε : ℝ)
(ε_pos : 0 < ε)
{ϕ : X → ℝ} :