English
If Tendsto (g ∘ f) a c and comap g c ≤ b, then Tendsto f a b.
Русский
Если Tendsto (g ∘ f) a c и comap g c ≤ b, то Tendsto f a b.
LaTeX
$$$\\forall f:\\alpha \\to \\beta, \\forall g:\\beta \\to \\gamma, \\forall a:\\mathrm{Filter}(\\alpha), \\forall b:\\mathrm{Filter}(\\beta), \\forall c:\\mathrm{Filter}(\\gamma),\\; \\mathrm{Tendsto}(g \\circ f)\\ a\\ c \\land (\\mathrm{comap}\\ g\\ c \\le b) \\Rightarrow \\mathrm{Tendsto} f\\ a\\ b$$$
Lean4
theorem of_tendsto_comp {f : α → β} {g : β → γ} {a : Filter α} {b : Filter β} {c : Filter γ} (hfg : Tendsto (g ∘ f) a c)
(hg : comap g c ≤ b) : Tendsto f a b := by
rw [tendsto_iff_comap] at hfg ⊢
calc
a ≤ comap (g ∘ f) c := hfg
_ ≤ comap f b := by simpa [comap_comap] using comap_mono hg
