measure_of_measure_compl_eq_zero — Mathlib

English

If ρ is a measure on α×β that is either zero or a probability measure, then the second marginal ρ.snd is also zero or a probability measure.

Русский

Если мера ρ на α×β равна нулю или является распределением вероятности, то ее вторичная маргинальная мера ρ.snd также равна нулю или распределению вероятности.

LaTeX

$$$\text{IsZeroOrProbabilityMeasure}(\rho) \Rightarrow \text{IsZeroOrProbabilityMeasure}(\rho_{\mathrm{snd}}).$$$

Lean4

theorem measure_of_measure_compl_eq_zero (hs : μ sᶜ = 0) : μ s = μ Set.univ := by
  simpa [hs] using measure_add_measure_compl₀ <| .of_compl <| .of_null hs

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