congr_right — Mathlib

English

Let μ be a measure on α and E a metric space. If g is μ-almost everywhere equal to g', and f converges to g in measure along l, then f converges to g' in measure along l.

Русский

Пусть μ — мера на α, E — метрическое пространство. Если g =μ-a.e. g', и f сходится по мере к g вдоль фильтра l, то f сходится по мере к g' вдоль l.

LaTeX

$$$\left(g =_{\mu} g'\right) \\Rightarrow TendstoInMeasure\;\mu\;f\;l\;g \\Rightarrow TendstoInMeasure\;\mu\;f\;l\;g'$$$

Lean4

theorem congr_right (h : g =ᵐ[μ] g') (h_tendsto : TendstoInMeasure μ f l g) : TendstoInMeasure μ f l g' :=
  h_tendsto.congr (fun _ => EventuallyEq.rfl) h

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