English
A variant that expresses IsLittleOTVS via smallSets around the origin; the relation is equivalent to a family of bounded comparisons against nested small sets.
Русский
Вариант выражения IsLittleOTVS через smallSets вокруг нуля; отношение эквивалентно семье ограничений по отношению к вложенным малым множествам.
LaTeX
$$$\\text{IsLittleOTVS}(\\\\mathfrak{k}, l, f, g) \\iff \\forall U \\in 𝓝(0_E), \\; \\forall V \\in (𝓝(0_E)).smallSets, \\; \\forall ε>0:\\; ∀ᶠ x\\in l, egauge(\\\\mathfrak{k}, U, f(x)) \\le ε \\cdot egauge(\\\\mathfrak{k}, V, g(x)).$$$
Lean4
theorem isLittleOTVS_iff_smallSets :
f =o[𝕜; l] g ↔
∀ U ∈ 𝓝 0, ∀ᶠ V in (𝓝 0).smallSets, ∀ ε ≠ (0 : ℝ≥0), ∀ᶠ x in l, egauge 𝕜 U (f x) ≤ ε * egauge 𝕜 V (g x) :=
(isLittleOTVS_iff ..).trans <|
forall₂_congr fun U hU ↦
.symm <| eventually_smallSets' fun V₁ V₂ hV hV₂ ε hε ↦ (hV₂ ε hε).mono fun x hx ↦ hx.trans <| by gcongr
