fst — Mathlib

English

For a measure ρ on α × β, the marginal on α is defined by ρ.fst(A) = ρ(Prod.fst^{-1}(A)) for all measurable A ⊆ α.

Русский

Для меры ρ на α × β маргинальная по α определяется как ρ.fst(A) = ρ(Prod.fst^{-1}(A)) для всех измеримых A ⊆ α.

LaTeX

$$$$\\rho.fst(A) = \\rho\\bigl(\\mathrm{Prod.fst}^{-1}(A)\\bigr)\\quad\\text{для всех измеримых }A\\subseteq\\alpha.$$$$

Lean4

/-- Marginal measure on `α` obtained from a measure `ρ` on `α × β`, defined by `ρ.map Prod.fst`. -/
noncomputable def fst (ρ : Measure (α × β)) : Measure α :=
  ρ.map Prod.fst

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