English
Convergence in measure is almost everywhere unique: if f converges to g and also to h in measure with respect to the same μ and f, then g = h μ-almost everywhere.
Русский
Сходимость по мере единственна почти наверняка: если f сходится по мере к g и к h по той же μ и к той же функции, то g = h μ-почти везде.
LaTeX
$$$[TendstoInMeasure\;\mu\;f\;u\;g] \wedge [TendstoInMeasure\;\mu\;f\;u\;h] \Rightarrow g =_{\mu} h$$$
Lean4
/-- The limit in measure is ae unique. -/
theorem tendstoInMeasure_ae_unique [EMetricSpace E] {g h : α → E} {f : ι → α → E} {u : Filter ι} [NeBot u]
[IsCountablyGenerated u] (hg : TendstoInMeasure μ f u g) (hh : TendstoInMeasure μ f u h) : g =ᵐ[μ] h :=
by
obtain ⟨ns, h1, h1'⟩ := hg.exists_seq_tendsto_ae'
obtain ⟨ns', h2, h2'⟩ := (hh.comp h1).exists_seq_tendsto_ae'
filter_upwards [h1', h2'] with ω hg1 hh1
exact tendsto_nhds_unique (hg1.comp h2) hh1
