tendsto_smallSets — Mathlib

English

Same as above; a simp version of tendsto_image_smallSets.

Русский

То же самое; упрощённая версия tendsto_image_smallSets.

LaTeX

$$$ \\forall {\\alpha} {\\beta} {l} {l'} {f}, \\; \\operatorname{Tendsto} (fun x => Set.image f x) l.smallSets l'.smallSets \\iff \\operatorname{Tendsto} f l l'. $$$

Lean4

theorem tendsto_smallSets {ι} [Preorder ι] {s : ι → Set α} (hl : l.HasAntitoneBasis s) : Tendsto s atTop l.smallSets :=
  tendsto_smallSets_iff.2 fun _t ht => hl.eventually_subset ht

Похожие утверждения