toMeasurable — Mathlib

English

If X is uniform on s with respect to μ and ℙ, then X is uniform on the measurable hull of s with the same parameters.

Русский

Если X равномерен на s относительно μ и ℙ, то X равномерен на измеримой оболочке s с теми же параметрами.

LaTeX

$$$\\text{IsUniform}(X, toMeasurable\\,\\mu s, \\mathbb{P}, \\mu)\\;\\text{from}\\; \\text{IsUniform}(X, s, \\mathbb{P}, \\mu)$$$

Lean4

protected theorem toMeasurable {X : Ω → E} {s : Set E} (hu : IsUniform X s ℙ μ) : IsUniform X (toMeasurable μ s) ℙ μ :=
  by
  unfold IsUniform at *
  rwa [ProbabilityTheory.cond_toMeasurable_eq]

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