English
IsLittleOTVS can be characterized via HasBasis descriptions at the origin: comparing gauges with respect to balanced neighborhoods around 0 provides a complete equivalence.
Русский
IsLittleOTVS можно охарактеризовать через описания HasBasis около нуля: сравнение gauges по сбалансированным окрестностям нуля обеспечивает эквивалентность.
LaTeX
$$$\\text{IsLittleOTVS}(\\\\mathfrak{k}, l, f, g) \\iff \\forall i, p_E(i) \\Rightarrow \\exists j, p_F(j) \\wedge (\\\\forall \\\\varepsilon \\\\in NNReal, \\\\varepsilon > 0 \\,\\\\Rightarrow \\,\\\\Eventually_{x \\to l} \, egauge(\\\\mathfrak{k}, s_E(i), f(x)) \\le \varepsilon \\, egauge(\\\\mathfrak{k}, s_F(j), g(x))).$$$
Lean4
protected theorem _root_.Filter.HasBasis.isLittleOTVS_iff {ιE ιF : Sort*} {pE : ιE → Prop} {pF : ιF → Prop}
{sE : ιE → Set E} {sF : ιF → Set F} (hE : HasBasis (𝓝 (0 : E)) pE sE) (hF : HasBasis (𝓝 (0 : F)) pF sF) :
f =o[𝕜; l] g ↔
∀ i, pE i → ∃ j, pF j ∧ ∀ ε ≠ (0 : ℝ≥0), ∀ᶠ x in l, egauge 𝕜 (sE i) (f x) ≤ ε * egauge 𝕜 (sF j) (g x) :=
by
rw [isLittleOTVS_iff]
refine (hE.forall_iff ?_).trans <| forall₂_congr fun _ _ ↦ hF.exists_iff ?_
· rintro s t hsub ⟨V, hV₀, hV⟩
exact ⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x ↦ le_trans <| egauge_anti _ hsub _⟩
· refine fun s t hsub h ε hε ↦ (h ε hε).mono fun x hx ↦ hx.trans ?_
simp only
gcongr
