tendsto_ae_unique — Mathlib

English

The ae-limit is ae-unique: if for almost every ω Tendsto(f i ω) to g(ω) and to h(ω), then g =ᵐ μ h.

Русский

Ae-граничение уникально: если практически для почти всех ω стремление f i ω к g(ω) и к h(ω), то g =ᵐ μ h.

LaTeX

$$$\\text{tendsto\_nhds\_unique}(hg, hh) \\Rightarrow g =^{\\mu} h$$$

Lean4

/-- The ae-limit is ae-unique. -/
theorem tendsto_ae_unique {ι : Type*} [T2Space β] {g h : α → β} {f : ι → α → β} {l : Filter ι} [l.NeBot]
    (hg : ∀ᵐ ω ∂μ, Tendsto (fun i => f i ω) l (𝓝 (g ω))) (hh : ∀ᵐ ω ∂μ, Tendsto (fun i => f i ω) l (𝓝 (h ω))) :
    g =ᵐ[μ] h := by filter_upwards [hg, hh] with ω hg1 hh1 using tendsto_nhds_unique hg1 hh1

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