tendsto_nhds_iff — Mathlib

English

If f is a closed embedding, then for any g, l, and x, Tendsto g l (𝓝 x) iff Tendsto (f ∘ g) l (𝓝 (f x)).

Русский

Если f — замкнутое вложение, тогда для любых g, фильтра l и точки x имеет место равенство тензорности несущейся: Tendsto g l (𝓝 x) ⇔ Tendsto (f ∘ g) l (𝓝 (f x)).

LaTeX

$$$\mathrm{IsClosedEmbedding}(f) \rightarrow \Big( \mathrm{Tendsto}(g, l, \mathcal{N}(x)) \leftrightarrow \mathrm{Tendsto}(f \circ g, l, \mathcal{N}(f(x))) \Big)$$$

Lean4

theorem tendsto_nhds_iff {g : ι → X} {l : Filter ι} {x : X} (hf : IsClosedEmbedding f) :
    Tendsto g l (𝓝 x) ↔ Tendsto (f ∘ g) l (𝓝 (f x)) :=
  hf.isEmbedding.tendsto_nhds_iff

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