tendsto_coe' — Mathlib

English

For a filtered space with NeBot, Tendsto (a ↦ m a) f (𝓝 x) is equivalent to the existence of hx ≥ 0 with Tendsto m f (𝓝 ⟨x, hx⟩).

Русский

При не пустом фильтре существуют hx ≥ 0 такие, что Tendsto m f (𝓝 ⟨x, hx⟩).

LaTeX

$$$\\text{Tendsto} (a \\mapsto m a)\\ f\\ (\\mathcal{N} x) \\iff \\exists hx : 0 \\le x, \\text{Tendsto} \\ m\\ f\\ (\\mathcal{N} \\langle x, hx \\rangle)$$$

Lean4

theorem tendsto_coe' {f : Filter α} [NeBot f] {m : α → ℝ≥0} {x : ℝ} :
    Tendsto (fun a => m a : α → ℝ) f (𝓝 x) ↔ ∃ hx : 0 ≤ x, Tendsto m f (𝓝 ⟨x, hx⟩) :=
  ⟨fun h => ⟨ge_of_tendsto' h fun c => (m c).2, tendsto_coe.1 h⟩, fun ⟨_, hm⟩ => tendsto_coe.2 hm⟩

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