English
If NullMeasurableSet sᶜ μ then NullMeasurableSet s μ.
Русский
Если sᶜ является NullMeasurableSet по μ, то и s является NullMeasurableSet по μ.
LaTeX
$$$$ \\text{NullMeasurableSet }(s^{c}) \\Rightarrow \\text{NullMeasurableSet }(s). $$$$
Lean4
theorem disjoint_of_disjoint_ae (h : Disjoint (ae μ) (ae ν)) : Disjoint μ ν :=
by
rw [disjoint_iff_inf_le] at h ⊢
refine Measure.le_intro fun s hs _ ↦ ?_
rw [Measure.inf_apply hs]
have : (⊥ : Measure α) = 0 := rfl
simp only [this, Measure.coe_zero, Pi.zero_apply, nonpos_iff_eq_zero]
specialize h (mem_bot (s := sᶜ))
rw [mem_inf_iff] at h
obtain ⟨t₁, ht₁, t₂, ht₂, h_eq'⟩ := h
have h_eq : s = t₁ᶜ ∪ t₂ᶜ := by rw [union_eq_compl_compl_inter_compl, compl_compl, compl_compl, ← h_eq', compl_compl]
rw [mem_ae_iff] at ht₁ ht₂
refine le_antisymm ?_ zero_le'
refine sInf_le_of_le (a := 0) (b := 0) ?_ le_rfl
rw [h_eq]
refine ⟨t₁ᶜ ∩ t₂, Eq.symm ?_⟩
rw [add_eq_zero]
constructor
· refine measure_inter_null_of_null_left _ ?_
exact measure_inter_null_of_null_left _ ht₁
· rw [compl_inter, compl_compl, union_eq_compl_compl_inter_compl, union_eq_compl_compl_inter_compl, ← compl_union,
compl_compl, compl_compl, inter_comm, inter_comm t₁, union_comm, inter_union_compl]
exact ht₂
