iUnion_negAt_plusPart_ae — Mathlib

English

If A is symmetric at real places, then the union over s of negAt s '' (plusPart A) is equal to A almost everywhere with respect to volume: ⋃ s negAt s '' plusPart A =ᵐ[volume] A.

Русский

Если A симметрично по вещественным местам, то объединение несёт тот же объем и эквивалентно A почти везде по мере: ⋃ s negAt s '' plusPart A =ᵐ[volume] A.

LaTeX

$$⋃_s negAt(s)''(plusPart(A)) =ᵐ[volume] A$$

Lean4

theorem iUnion_negAt_plusPart_ae : ⋃ s, negAt s '' (plusPart A) =ᵐ[volume] A :=
  by
  nth_rewrite 2 [← iUnion_negAt_plusPart_union A hA]
  refine (MeasureTheory.union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)).symm
  exact measure_mono_null Set.inter_subset_right (measure_iUnion_null_iff.mpr fun _ ↦ volume_eq_zero _)

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