English
For any measurable space and measure μ on 𝓧, there exists Ω, a measurable structure, a measure P on Ω, and a measurable X: Ω → 𝓧 with HasLaw X μ P.
Русский
Для любого измеримого пространства и меры μ на 𝓧 существует пространство Ω с измеримой структурой, мера P на Ω и измеримое отображение X: Ω → 𝓧 с HasLaw X μ P.
LaTeX
$$$$ \\exists \\Omega, \\exists mΩ, \\exists P, \\exists X : \\Omega \\to 𝓧, \\text{Measurable } X \\; \\land \\text{HasLaw } X \\; μ \\; P $$$$
Lean4
theorem _root_.Measure.exists_hasLaw {𝓧 : Type u} {m𝓧 : MeasurableSpace 𝓧} (μ : Measure 𝓧) :
∃ Ω : Type u, ∃ _ : MeasurableSpace Ω, ∃ P : Measure Ω, ∃ X : Ω → 𝓧, Measurable X ∧ HasLaw X μ P :=
⟨𝓧, m𝓧, μ, id, measurable_id, .id⟩
