ae_restrict_biUnion_finset_iff — Mathlib

English

The equality of almost-everywhere restrictions is equivalent to equality of almost-everywhere restrictions on each component of the union.

Русский

Равенство a.e. ограничений на объединение эквивалентно равенству на каждом компоненте объединения.

LaTeX

$$$f =ᵐ[μ.restrict (\\bigcup_{i} s_i)] g \\iff \\forall i, f =ᵐ[μ.restrict (s_i)] g$.$$

Lean4

@[simp]
theorem ae_restrict_biUnion_finset_iff (s : ι → Set α) (t : Finset ι) (p : α → Prop) :
    (∀ᵐ x ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ x ∂μ.restrict (s i), p x := by
  simp_rw [Filter.Eventually, ae_restrict_biUnion_finset_eq s, mem_iSup]

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