hasLaw — Mathlib

English

If a map X is measure-preserving from P to μ, then X has a law with respect to μ and P.

Русский

Если отображение X сохраняет меру от P к μ, тогда X имеет закон по отношению к μ и P.

LaTeX

$$$$ \\text{MeasurePreserving } X\\; P\\; \\mu \\Rightarrow \\HasLaw\\; X\\; \\mu\\; P $$$$

Lean4

theorem _root_.MeasureTheory.MeasurePreserving.hasLaw (h : MeasurePreserving X P μ) : HasLaw X μ P
    where
  aemeasurable := h.measurable.aemeasurable
  map_eq := h.map_eq

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