comp — Mathlib

English

If a.e. equality holds for sequences f_i ↔ f_i' and g ≡ g' almost everywhere, TendstoInMeasure is preserved under those a.e. replacements.

Русский

Если для последовательностей выполняются эквивалентности almost everywhere, то TendstoInMeasure сохраняется при заменах на эквивалентные almost everywhere функции.

LaTeX

$$$(h_left: ∀ᶠ i in l, f_i =ᵐ[μ] f'_i) (h_right: g =ᵐ[μ] g') (h_tendsto: TendstoInMeasure μ f l g) \\Rightarrow TendstoInMeasure μ f' l g'$$$

Lean4

theorem comp [EDist E] {f : ι → α → E} {g : α → E} {u : Filter ι} {v : Filter κ} {ns : κ → ι}
    (hg : TendstoInMeasure μ f u g) (hns : Tendsto ns v u) : TendstoInMeasure μ (f ∘ ns) v g := fun ε hε ↦
  (hg ε hε).comp hns

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