tendsto_nhds_iff' — Mathlib

English

Let hf be an open embedding. Then Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l.

Русский

Пусть hf — открытое вложение. Тогда Tendsto (g ∘ f) (nhds x) l ↔ Tendsto g (nhds (f x)) l.

LaTeX

$$$ \operatorname{Tendsto} (g \circ f) (\mathcal{N}x) l \iff \operatorname{Tendsto} g (\mathcal{N}(f x)) l $$$

Lean4

theorem tendsto_nhds_iff' (hf : IsOpenEmbedding f) {l : Filter Z} {x : X} :
    Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l := by rw [Tendsto, ← map_map, hf.map_nhds_eq]; rfl

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