tendsto_toNNReal_iff' — Mathlib

English

If f and g are ENNReal-valued with f x ≠ ∞ and g x ≠ ∞ eventually, and (f x).toReal = (g x).toReal eventually, then f =ᶠ g.

Русский

Если f и g сходятся до Real в пределах ENNReal и равны по toReal почти везде, то f =ᶠ g.

LaTeX

$$$\\bigl( \\forall^{\\infty} x, f(x) \\neq \\infty \\bigr) \\land \\bigl( \\forall^{\\infty} x, g(x) \\neq \\infty \\bigr) \\land \\bigl( (f(x)).toReal = (g(x)).toReal \\bigr) \\Rightarrow f =^{\\infty}_{l} g$$$

Lean4

theorem tendsto_toNNReal_iff' {f : α → ℝ≥0∞} {u : Filter α} {a : ℝ≥0} (hf : ∀ x, f x ≠ ∞) :
    Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a) ↔ Tendsto f u (𝓝 a) :=
  by
  rw [← toNNReal_coe a]
  exact tendsto_toNNReal_iff coe_ne_top hf

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