English
For any binary operation op with ∥op(x,y)∥ ≤ ∥x∥∥y∥, and for f, g as in the previous lemma with f tending to 1 and g bounded, there is a radius condition ensuring r < ∥x∥ implies ε < ∥f(x)∥ etc.
Русский
Для любой двоичной операции с условием ∥op(x,y)∥ ≤ ∥x∥∥y∥, справедливое при f→1 и bounded g, существует граница, после которой контроль нормы обеспечивает требуемый предел.
LaTeX
$$$\exists r:\ \mathbb{R},\forall x:\ E,\ r<\|x\| \Rightarrow \varepsilon < \|f(x)\|$$$
Lean4
theorem norm_le [ProperSpace F] [FunLike 𝓕 E F] [CocompactMapClass 𝓕 E F] (ε : ℝ) :
∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖ := by
have h := cocompact_tendsto f
rw [tendsto_def] at h
specialize h (Metric.closedBall 0 ε)ᶜ (mem_cocompact_of_closedBall_compl_subset 0 ⟨ε, rfl.subset⟩)
rcases closedBall_compl_subset_of_mem_cocompact h 0 with ⟨r, hr⟩
use r
intro x hx
suffices x ∈ f ⁻¹' (Metric.closedBall 0 ε)ᶜ by simp_all
apply hr
simp [hx]
