disjoint — Mathlib

English

If μ ⟂ ν, then Disjoint (ae μ) (ae ν).

Русский

Если μ ⟂ₘ ν, то Disjoint (ae μ) (ae ν).

LaTeX

$$$$ \\mu \\perp_{m} \\nu \\Rightarrow \\; \\text{Disjoint} (\\ae \\mu) (\\ae \\nu). $$$$

Lean4

theorem disjoint (h : μ ⟂ₘ ν) : Disjoint μ ν :=
  by
  have h_bot_iff (ξ : Measure α) : ξ ≤ ⊥ ↔ ξ = 0 := by
    rw [le_bot_iff]
    rfl
  intro ξ hξμ hξν
  rw [h_bot_iff]
  ext s hs
  simp only [Measure.coe_zero, Pi.zero_apply]
  rw [← inter_union_compl s h.nullSet, measure_union, add_eq_zero]
  ·
    exact
      ⟨measure_inter_null_of_null_right _ <| absolutelyContinuous_of_le hξμ h.measure_nullSet,
        measure_inter_null_of_null_right _ <| absolutelyContinuous_of_le hξν h.measure_compl_nullSet⟩
  · exact Disjoint.mono inter_subset_right inter_subset_right disjoint_compl_right
  · exact hs.inter h.measurableSet_nullSet.compl

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