eventuallyEq_of_toReal_eventuallyEq

English

For a function hf: ∀ x, f x ≠ ∞, (tendsto toNNReal ∘ f) u (nhds a) iff Tendsto f u (nhds a) for ENNReal.

Русский

Для функции f с условием f x ≠ ∞ выполняется эквивалентность перехода toNNReal ∘ f к a и перехода f к a.

LaTeX

$$$\\operatorname{Tendsto}(\\mathrm{ENNReal}.toNNReal \\circ f) u (\\mathcal{N}(a)) \\iff \\operatorname{Tendsto} f u (\\mathcal{N}(a))$$$

Lean4

theorem eventuallyEq_of_toReal_eventuallyEq {l : Filter α} {f g : α → ℝ≥0∞} (hfi : ∀ᶠ x in l, f x ≠ ∞)
    (hgi : ∀ᶠ x in l, g x ≠ ∞) (hfg : (fun x => (f x).toReal) =ᶠ[l] fun x => (g x).toReal) : f =ᶠ[l] g :=
  by
  filter_upwards [hfi, hgi, hfg] with _ hfx hgx _
  rwa [← ENNReal.toReal_eq_toReal hfx hgx]

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