tendsto_map'_iff — Mathlib

English

For f: γ → δ, g: α → β, Tendsto f (map g x) y iff Tendsto (f ∘ g) x y.

Русский

Для f: γ → δ, g: α →β, Tendsto f (map g x) y эквивалентно Tendsto (f ∘ g) x y.

LaTeX

$$$\\forall f:\\gamma \\to \\delta, \\forall g:\\alpha \\to \\beta, \\forall x:\\mathrm{Filter}(\\alpha), \\forall y:\\mathrm{Filter}(\\gamma),\\; \\mathrm{Tendsto} f (\\mathrm{map} g\\ x) y \\iff \\mathrm{Tendsto} (f \\circ g) x y$$$

Lean4

@[simp]
theorem tendsto_map'_iff {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ} :
    Tendsto f (map g x) y ↔ Tendsto (f ∘ g) x y := by rw [Tendsto, Tendsto, map_map]

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