tendsto_coe — Mathlib

English

Tendsto (ENNReal.ofNNReal ∘ m) to ENNReal at a equals Tendsto m to a in NNReal.

Русский

Сходимость отображения ENNReal.ofNNReal ∘ m эквивалентна сходимости m в NNReal.

LaTeX

$$$\forall f\, \forall m\, \forall a:\, \text{Tendsto} (\lambda a. ENNReal.ofNNReal (m a)) f (\mathcal{N}(\text{ENNReal.ofNNReal } a)) \iff \text{Tendsto} m f (\mathcal{N}(a)).$$$

Lean4

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

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