ae_eq_pi — Mathlib

English

If f_i =ᵐ[μ_i] f'_i for all i, then the coordinatewise composed map x ↦ f_i(x_i) equalsᵐ[π μ] the map x ↦ f'_i(x_i).

Русский

Если для всех i верно f_i =ᵐ f'_i по μ_i, то функция x ↦ f_i(x_i) равна по мере π μ функции x ↦ f'_i(x_i).

LaTeX

$$(∀ i, f i =ᵐ[μ i] f' i) → (fun (x) i => f i (x i)) =ᵐ[π μ] fun x i => f' i (x i)$$

Lean4

theorem ae_eq_pi {β : ι → Type*} {f f' : ∀ i, α i → β i} (h : ∀ i, f i =ᵐ[μ i] f' i) :
    (fun (x : ∀ i, α i) i => f i (x i)) =ᵐ[Measure.pi μ] fun x i => f' i (x i) :=
  (eventually_all.2 fun i => tendsto_eval_ae_ae.eventually (h i)).mono fun _ hx => funext hx

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