ae_le_pi — Mathlib

English

If f_i ≤ᵐ[μ_i] f'_i for all i, then the corresponding product map is ≤ᵐ[π μ] pointwise.

Русский

Если f_i ≤ᵐ[μ_i] f'_i для всех i, то соответствующая карта произведения удовлетворяет ≤ᵐ по π μ точечно.

LaTeX

$$$ (\forall i, f i ≤ᵐ[μ i] f' i) \Rightarrow (\lambda x i. f i (x i)) ≤ᵐ[\pi μ] (\lambda x i. f' i (x i)) $$$

Lean4

theorem ae_le_pi {β : ι → Type*} [∀ i, Preorder (β i)] {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 => hx

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