English
Let f be a function from α to Set β. Then f converges to lb.smallSets along la if and only if for every t in lb, f(x) ⊆ t eventually as x tends along la.
Русский
Пусть f: α → Set β. Тогда сходимость f к lb.smallSets вдоль la эквивалентна тому, что для любого t ∈ lb, невыражено выполняется f(x) ⊆ t при x, стремящемся вдоль la.
LaTeX
$$$ \\forall f:\\\\alpha \\\\to \\\\mathcal P(\\\\beta),\\\\, \\operatorname{Tendsto} f \\\\la lb.smallSets \\\\iff \\\\forall t \\\\in lb, \\\\forall^\\\\infty x \\\\in la, \\\\ f(x) \\subset t $$$
Lean4
/-- `g` converges to `f.smallSets` if for all `s ∈ f`, eventually we have `g x ⊆ s`. -/
theorem tendsto_smallSets_iff {f : α → Set β} : Tendsto f la lb.smallSets ↔ ∀ t ∈ lb, ∀ᶠ x in la, f x ⊆ t :=
(hasBasis_smallSets lb).tendsto_right_iff
