English
If a function f: E → F satisfies ∀ ε > 0, ∃ r > 0 with ∀ x, r < ∥x∥ ⇒ ε < ∥f(x)∥, then f is Tendsto cocompact E to cocompact F.
Русский
Если функция f: E → F удовлетворяет ∀ ε>0, ∃ r>0: ∀ x, r < ∥x∥ ⇒ ε < ∥f(x)∥, то f является пределом в кококомпактном смысле.
LaTeX
$$$\forall ε>0,\ exists\ r>0,\forall x:\ r<\|x\| \Rightarrow \varepsilon < \|f(x)\| \implies f:\ \text{cocompact } E \to \text{cocompact } F$$$
Lean4
theorem tendsto_cocompact_cocompact_of_norm [ProperSpace E] {f : E → F}
(h : ∀ ε : ℝ, ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖) : Tendsto f (cocompact E) (cocompact F) :=
by
rw [tendsto_def]
intro s hs
rcases closedBall_compl_subset_of_mem_cocompact hs 0 with ⟨ε, hε⟩
rcases h ε with ⟨r, hr⟩
apply mem_cocompact_of_closedBall_compl_subset 0
use r
intro x hx
simp only [Set.mem_compl_iff, Metric.mem_closedBall, dist_zero_right, not_le] at hx
apply hε
simp [hr x hx]
