Documentation

Mathlib.Analysis.Normed.Group.CocompactMap

Cocompact maps in normed groups #

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

Main statements #

theorem CocompactMapClass.norm_le {E : Type u_2} {F : Type u_3} {𝓕 : Type u_4} [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_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [ProperSpace E] {f : EF} (h : ∀ (ε : ), ∃ (r : ), ∀ (x : E), r < xε < f x) :
theorem ContinuousMapClass.toCocompactMapClass_of_norm {E : Type u_2} {F : Type u_3} {𝓕 : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [ProperSpace E] [FunLike 𝓕 E F] [ContinuousMapClass 𝓕 E F] (h : ∀ (f : 𝓕) (ε : ), ∃ (r : ), ∀ (x : E), r < xε < f x) :