nhds — Mathlib

English

Let f: α → X and l be a filter on α. If f tends to nhds x, then nhds ∘ f tends to nhds (nhds x).

Русский

Пусть f: α → X и l — фильтр на α. Если f стремится к 𝓝 x, то 𝓝 ∘ f стремится к 𝓝(𝓝 x).

LaTeX

$$$\\operatorname{Tendsto}(f,l,\\mathcal{N}x)\\Rightarrow\\operatorname{Tendsto}(\\mathcal{N}\\circ f)\\,l\\,\\mathcal{N}(\\mathcal{N}x)$$$

Lean4

protected theorem nhds {f : α → X} {l : Filter α} {x : X} (h : Tendsto f l (𝓝 x)) : Tendsto (𝓝 ∘ f) l (𝓝 (𝓝 x)) :=
  (continuous_nhds.tendsto _).comp h

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