ZeroAtInftyContinuousMapClass in normed additive groups

In this file we give a characterization of the predicate zero_at_infty from ZeroAtInftyContinuousMapClass. A continuous map f is zero at infinity if and only if for every ε > 0 there exists a r : ℝ such that for all x : E with r < ‖x‖ it holds that ‖f x‖ < ε.

theorem ZeroAtInftyContinuousMapClass.norm_le {E : Type u_1} {F : Type u_2} {𝓕 : Type u_3} [SeminormedAddGroup E] [SeminormedAddCommGroup F] [FunLike 𝓕 E F] [ZeroAtInftyContinuousMapClass 𝓕 E F] (f : 𝓕) (ε : ℝ) (hε : 0 < ε) : ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε

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