isProbabilityMeasure — Mathlib

English

Independence of a family implies that the underlying measure is a probability measure when the base is a probability space.

Русский

Независимость семейства влечёт ему быть вероятностной мерой в базовом вероятностном пространстве.

LaTeX

$$$iIndep m μ \Rightarrow IsProbabilityMeasure μ$$

Lean4

theorem isProbabilityMeasure (h : iIndep m μ) : IsProbabilityMeasure μ :=
  h.iIndepSets'.isProbabilityMeasure

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