toMeasurable_iff — Mathlib

English

X is uniform on the measurable hull of s if and only if X is uniform on s itself.

Русский

X равномерно по s тогда и только тогда, когда X равномерно по единице измерения, ограниченной на её замкнутый (toMeasurable) набор.

LaTeX

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

Lean4

theorem toMeasurable_iff {X : Ω → E} {s : Set E} : IsUniform X (toMeasurable μ s) ℙ μ ↔ IsUniform X s ℙ μ :=
  by
  unfold IsUniform
  rw [ProbabilityTheory.cond_toMeasurable_eq]

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