fst_univ — Mathlib

English

The first marginal of a measure on α × β evaluated at the whole space equals the measure of the whole space: ρ.fst univ = ρ univ.

Русский

Первая маргинальная мера на α×β, применённая к весь пространству, равна мере самой меры: ρ.fst univ = ρ univ.

LaTeX

$$$$\\rho.fst(\\mathrm{univ}) = \\rho(\\mathrm{univ})$$$$

Lean4

theorem fst_univ : ρ.fst univ = ρ univ := by rw [fst_apply MeasurableSet.univ, preimage_univ]

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