instIsProbabilityMeasureToFiniteOfNeZeroMeasure

English

If μ is SFinite, μ.toFinite is a probability measure provided μ ≠ 0.

Русский

Если μ является SFinite и μ ≠ 0, то μ.toFinite — вероятностьная мера.

LaTeX

$$$ [SFinite μ] [NeZero μ] \Rightarrow IsProbabilityMeasure(μ^{toFinite}) $$$

Lean4

instance [SFinite μ] [NeZero μ] : IsProbabilityMeasure μ.toFinite :=
  by
  apply ProbabilityTheory.cond_isProbabilityMeasure
  simp [ne_eq, ← compl_mem_ae_iff, ae_toFiniteAux]

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