tendsto_coe — Mathlib

English

Tendsto (a ↦ (m a : ℝ)) f (𝓝 x) is equivalent to Tendsto m f (𝓝 x) for m : α → ℝ≥0.

Русский

Сходимость (м:s) через вещественное отображение эквивалентна исходной сходимости m.

LaTeX

$$$\\text{Tendsto} (a \\mapsto (m a : \\mathbb{R}))\ f\\ (\\mathcal{N}(x)) \\iff \\text{Tendsto} \\, m\\ f\\ (\\mathcal{N} x)$$$

Lean4

@[simp, norm_cast]
theorem tendsto_coe {f : Filter α} {m : α → ℝ≥0} {x : ℝ≥0} :
    Tendsto (fun a => (m a : ℝ)) f (𝓝 (x : ℝ)) ↔ Tendsto m f (𝓝 x) :=
  tendsto_subtype_rng.symm

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