English
The map sending a set to its image under f preserves tendsto along smallSets: Tendsto (f '' ·) la.smallSets lb.smallSets iff Tendsto f la lb.
Русский
Отображение множества через f сохраняет сходимость вдоль smallSets: Tendsto (f '' ·) la.smallSets lb.smallSets эквивалентно Tendsto f la lb.
LaTeX
$$$ \\forall {f : \\alpha \\to \\beta},\\; \\\\operatorname{Tendsto} (f '' \\cdot) l.smallSets lb.smallSets \\\\iff \\\\operatorname{Tendsto} f l lb $$$
Lean4
@[simp]
theorem tendsto_image_smallSets {f : α → β} : Tendsto (f '' ·) la.smallSets lb.smallSets ↔ Tendsto f la lb :=
by
rw [tendsto_smallSets_iff]
refine forall₂_congr fun u hu ↦ ?_
rw [eventually_smallSets' fun s t hst ht ↦ (image_mono hst).trans ht]
simp only [image_subset_iff, exists_mem_subset_iff, mem_map]
