disjoint_ae — Mathlib

English

NullMeasurable(A ∁) iff NullMeasurable(A).

Русский

NullMeasurableSet(Aᶜ) эквивалентно NullMeasurableSet(A).

LaTeX

$$$$ \\text{NullMeasurableSet }(s^{c}) \\;\\iff\\; \\text{NullMeasurableSet }(s). $$$$

Lean4

theorem disjoint_ae (h : μ ⟂ₘ ν) : Disjoint (ae μ) (ae ν) :=
  by
  rw [disjoint_iff_inf_le]
  intro s _
  refine ⟨s ∪ h.nullSetᶜ, ?_, s ∪ h.nullSet, ?_, ?_⟩
  · rw [mem_ae_iff, compl_union, compl_compl]
    exact measure_inter_null_of_null_right _ h.measure_nullSet
  · rw [mem_ae_iff, compl_union]
    exact measure_inter_null_of_null_right _ h.measure_compl_nullSet
  ·
    rw [union_eq_compl_compl_inter_compl, union_eq_compl_compl_inter_compl, ← compl_union, compl_compl,
      inter_union_compl, compl_compl]

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