congr_left — Mathlib

English

Let μ be a measure on α and E a metric space. For each i in ι, let f_i, f'_i : α → E. If f_i and f'_i are μ-almost everywhere equal for every i, and f tends to g in measure along l, then f' tends to g in measure along l.

Русский

Пусть μ — мера на α, E — метрическое пространство. Пусть для каждого i ∈ ι функции f_i, f'_i : α → E удовлетворяют f_i =μ-a.e. f'_i. Если сборка f = (f_i) сходится по мере к g вдоль фильтра l, то сборка f' = (f'_i) тоже сходится по мере к g вдоль l.

LaTeX

$$$\\left(\\forall i,\, f_i =_{\\mu} f'_i\\right) \\\\Rightarrow TendstoInMeasure\\;\\mu\\;f\\;l\\;g \\\\Rightarrow TendstoInMeasure\\;\\mu\\;f'\\;l\\;g$$$

Lean4

theorem congr_left (h : ∀ i, f i =ᵐ[μ] f' i) (h_tendsto : TendstoInMeasure μ f l g) : TendstoInMeasure μ f' l g :=
  h_tendsto.congr h EventuallyEq.rfl

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