English
Big-OTVS has a similar HasBasis characterization: being O-relatively bounded by senses of gauges is equivalent to a family of small sets with a corresponding bound.
Русский
Big-OTVS имеет аналогичную характеристику HasBasis: быть ограниченным по отношению к масштабу gauge эквивалентно существованию семейства малых множеств с заданным пределом.
LaTeX
$$$\\text{IsBigOTVS}(\\\\mathfrak{k}, l, f, g) \\iff \\forall i, p_E(i) \\Rightarrow \\exists j, p_F(j) \\wedge \\forall \\; \\varepsilon>0:\\; \\text{Event}ําually_{x\\in l} \\; ENNReal.le(egauge(\\\\mathfrak{k}, s_E(i), f(x)), egauge(\\\\mathfrak{k}, s_F(j), g(x)) \\cdot \\\\varepsilon).$$$
Lean4
protected theorem _root_.Filter.HasBasis.isBigOTVS_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 ∧ ∀ᶠ x in l, egauge 𝕜 (sE i) (f x) ≤ egauge 𝕜 (sF j) (g x) :=
by
rw [isBigOTVS_iff]
refine (hE.forall_iff ?_).trans <| forall₂_congr fun _ _ ↦ hF.exists_iff ?_
· rintro s t hsub ⟨V, hV₀, hV⟩
exact ⟨V, hV₀, hV.mono fun x ↦ le_trans <| egauge_anti _ hsub _⟩
· exact fun s t hsub h ↦ h.mono fun x hx ↦ hx.trans <| egauge_anti 𝕜 hsub (g x)
