mathlib documentation


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.


theorem hofer {X : Type u_1} [metric_space X] [complete_space X] (x : X) (ε : ) (ε_pos : 0 < ε) {ϕ : X → } :
continuous ϕ(∀ (y : X), 0 ϕ y)(∃ (ε' : ) (H : ε' > 0) (x' : X), ε' ε dist x' x 2 * ε ε * ϕ x ε' * ϕ x' ∀ (y : X), dist x' y ε'ϕ y 2 * ϕ x')