union_ae_eq_left_iff_ae_subset — Mathlib

English

Let μ be a measure and s,t subsets. Then (s ∪ t) is μ-almost everywhere equal to s if and only if t is μ-almost contained in s; equivalently, μ(t \ s) = 0.

Русский

Пусть μ — мера и s,t подмножества. Тогда (s ∪ t) =ᵐμ s тогда и только тогда, когда t ≼μ s почти внутри s; эквивалентно μ(t \ s) = 0.

LaTeX

$$$ (s \cup t) =^{\mu}_{\mathrm{a.e.}} s \iff t \le^{\mu}_{\mathrm{a.e.}} s $$$

Lean4

@[simp]
theorem union_ae_eq_left_iff_ae_subset : (s ∪ t : Set α) =ᵐ[μ] s ↔ t ≤ᵐ[μ] s :=
  by
  rw [ae_le_set]
  refine
    ⟨fun h => by simpa only [union_diff_left] using (ae_eq_set.mp h).1, fun h =>
      eventuallyLE_antisymm_iff.mpr
        ⟨by rwa [ae_le_set, union_diff_left], HasSubset.Subset.eventuallyLE subset_union_left⟩⟩

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