ae_le_set_pi — Mathlib

English

If s_i ≤ᵐ[μ_i] t_i for all i in a finite index set I, then Set.pi I s ≤ᵐ[Measure.pi μ] Set.pi I t.

Русский

Если для всех i ∈ I s_i ≤ᵐ t_i по μ_i, то произведение множеств S ≤ᵐ по π μ.

LaTeX

$$$\forall s,t, (\forall i\in I, s_i \leq_{ae}^{\mu_i} t_i) \Rightarrow (\mathrm{Set.pi} I s) \leq_{ae}^{\pi\mu} (\mathrm{Set.pi} I t)$$$

Lean4

theorem ae_le_set_pi {I : Set ι} {s t : ∀ i, Set (α i)} (h : ∀ i ∈ I, s i ≤ᵐ[μ i] t i) :
    Set.pi I s ≤ᵐ[Measure.pi μ] Set.pi I t :=
  ((eventually_all_finite I.toFinite).2 fun i hi => tendsto_eval_ae_ae.eventually (h i hi)).mono fun _ hst hx i hi =>
    hst i hi <| hx i hi

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