English
For any f,g and hk, f = o_{𝕜;l} g if and only if for every neighborhood U of 0 there exists a neighborhood V of 0 such that egauge 𝕜 U (f x) / egauge 𝕜 V (g x) tends to 0 along l.
Русский
Для любых f,g и hk, f = o_{𝕜;l} g тогда и только тогда, когда для каждого окрестности U 0 существует окрестность V 0 так, что отношение egauge 𝕜 U (f x) / egauge 𝕜 V (g x) стремится к 0 вдоль l.
LaTeX
$$$f =o_{𝕜;l} g \\iff \\forall U \\in 𝓝(0),\\ \\exists V \\in 𝓝(0),\\ Tendsto\\bigl( x \\mapsto \\frac{egauge 𝕜 U (f x)}{egauge 𝕜 V (g x)} \\bigr)\\ l\\ (nhds\\ 0).$$$
Lean4
theorem isLittleOTVS_iff_tendsto_div :
f =o[𝕜; l] g ↔ ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, Tendsto (fun x ↦ egauge 𝕜 U (f x) / egauge 𝕜 V (g x)) l (𝓝 0) :=
by
simp only [isLittleOTVS_iff, ← ENNReal.coe_zero, ENNReal.nhds_coe, ← NNReal.bot_eq_zero,
(nhds_bot_basis_Iic.map _).tendsto_right_iff]
simp +contextual [ENNReal.div_le_iff_le_mul, pos_iff_ne_zero, EventuallyLE]
