tendsto_nhds_right — Mathlib

English

For f: β → α, a: α, Tendsto u f (𝓝 a) is equivalent to Tendsto (λ x, (a, u x)) f (𝓤 α).

Русский

Для f: β → α, a: α, Tendsto u f (𝓝 a) эквивалентно Tendsto (λ x, (a, u x)) f (𝓤 α).

LaTeX

$$$\\operatorname{Tendsto}(u\\,f\\, (\\mathcal{N}(a))) \\iff \\operatorname{Tendsto}(\\lambda x. (a, u x))\,f\, (\\mathcal{U}(\\alpha))$$$

Lean4

theorem tendsto_nhds_right {f : Filter β} {u : β → α} {a : α} :
    Tendsto u f (𝓝 a) ↔ Tendsto (fun x => (a, u x)) f (𝓤 α) := by rw [nhds_eq_comap_uniformity, tendsto_comap_iff]; rfl

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