measure_univ_eq_of_subset — Mathlib

English

For a projective family, the total mass over the whole index equals the mass over any subset projection.

Русский

Для проективной семейства масса по всему множеству индексов равна массе по любой проекции подмножества.

LaTeX

$$$P I\,\text{univ} = P J\,\text{univ}$ for suitable J ⊆ I.$$

Lean4

/-- Auxiliary lemma for `measure_univ_eq`. -/
theorem measure_univ_eq_of_subset (hP : IsProjectiveMeasureFamily P) (hJI : J ⊆ I) : P I univ = P J univ := by
  classical
  have : (univ : Set (∀ i : I, α i)) = Finset.restrict₂ hJI ⁻¹' (univ : Set (∀ i : J, α i)) := by rw [preimage_univ]
  rw [this, ← Measure.map_apply _ MeasurableSet.univ]
  · rw [hP I J hJI]
  · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

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