instIsZeroOrProbabilityMeasure — Mathlib

English

The second marginal of a measure on α×β is zero-or-probability if the original measure is zero-or-probability.

Русский

Вторичная маргинальная мера от меры на α×β имеет свойство ноль-или-вероятность, если исходная мера обладает этим свойством.

LaTeX

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

Lean4

instance instIsZeroOrProbabilityMeasure [IsZeroOrProbabilityMeasure ρ] : IsZeroOrProbabilityMeasure ρ.snd :=
  by
  rcases eq_zero_or_isProbabilityMeasure ρ with h | h
  · simp only [h, snd_zero]
    infer_instance
  · infer_instance

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