ae_isProbabilityMeasure — Mathlib

English

If h : iIndep m κ μ, then almost surely κ a is a probability measure.

Русский

Если выполнено iIndep m κ μ, то почти наверняка κ a — вероятность мера.

LaTeX

$$$ (h : iIndep m κ μ) \\Rightarrow \\forall^{{\\mathrm{ae}}} a \\partial μ, IsProbabilityMeasure (κ a) $$$

Lean4

theorem ae_isProbabilityMeasure (h : iIndep m κ μ) : ∀ᵐ a ∂μ, IsProbabilityMeasure (κ a) :=
  h.iIndepSets'.ae_isProbabilityMeasure

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