exists_eq_disjoint_finiteSpanningSetsIn

English

There exist S and T in FiniteSpanningSetsIn for μ and ν that share the same underlying set and are pairwise disjoint.

Русский

Существуют S и T в μ.FiniteSpanningSetsIn и ν.FiniteSpanningSetsIn с одинаковым основанием множества и попарно непересекающимися.

LaTeX

$$$\exists S: μ.FiniteSpanningSetsIn\{s\mid MeasurableSet s\} \exists T: ν.FiniteSpanningSetsIn\{s\mid MeasurableSet s\},\; S.set = T.set \land \text{Pairwise}(Disjoint\ on\ S.set)$$$

Lean4

theorem exists_eq_disjoint_finiteSpanningSetsIn (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
    ∃ (S : μ.FiniteSpanningSetsIn {s | MeasurableSet s}) (T : ν.FiniteSpanningSetsIn {s | MeasurableSet s}),
      S.set = T.set ∧ Pairwise (Disjoint on S.set) :=
  let S := (μ + ν).toFiniteSpanningSetsIn.disjointed
  ⟨S.ofLE (Measure.le_add_right le_rfl), S.ofLE (Measure.le_add_left le_rfl), rfl, disjoint_disjointed _⟩

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