ae_eq_restrict_biUnion_iff — Mathlib

English

The same as above, but with an equivalence of eventual equality rewritten in terms of iSup over finite sets.

Русский

То же самое для эквивалентности конвергенции почти всюду, переписанной через iSup по конечным множествам.

LaTeX

$$$f =ᵐ[μ.restrict (⋃ i ∈ t, s_i)] g \\iff ∀ i ∈ t, f =ᵐ[μ.restrict (s_i)] g$.$$

Lean4

theorem ae_eq_restrict_biUnion_iff (s : ι → Set α) {t : Set ι} (ht : t.Countable) (f g : α → δ) :
    f =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g ↔ ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g := by
  simp_rw [ae_restrict_biUnion_eq s ht, EventuallyEq, eventually_iSup]

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