Cocompact maps in normed groups

This file gives a characterization of cocompact maps in terms of norm estimates.

Main statements

• CocompactMapClass.norm_le: Every cocompact map satisfies a norm estimate
• ContinuousMapClass.toCocompactMapClass_of_norm: Conversely, this norm estimate implies that a map is cocompact.

theorem CocompactMapClass.norm_le {E : Type u_1} {F : Type u_2} {𝓕 : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : 𝓕} [ProperSpace F] [FunLike 𝓕 E F] [CocompactMapClass 𝓕 E F] (ε : ℝ) : ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖

theorem Filter.tendsto_cocompact_cocompact_of_norm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [ProperSpace E] {f : E → F} (h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖) : Tendsto f (cocompact E) (cocompact F)

theorem ContinuousMapClass.toCocompactMapClass_of_norm {E : Type u_1} {F : Type u_2} {𝓕 : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [ProperSpace E] [FunLike 𝓕 E F] [ContinuousMapClass 𝓕 E F] (h : ∀ (f : 𝓕) (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖) : CocompactMapClass 𝓕 E F