instIsZeroOrProbabilityMeasureMap

English

If μ is a zero-or-probability measure and f: α → β is any function, then the pushforward measure f_* μ is also zero-or-probability.

Русский

Пусть μ — нулевая или вероятностная мера; для любого отображения f: α → β мера, образованная по f, также нулевая или вероятностная.

LaTeX

$$$\mathrm{IsZeroOrProbabilityMeasure}(f_*\mu)$$$

Lean4

instance {f : α → β} : IsZeroOrProbabilityMeasure (map f μ) :=
  by
  by_cases hf : AEMeasurable f μ
  · simpa [isZeroOrProbabilityMeasure_iff, hf] using IsZeroOrProbabilityMeasure.measure_univ
  · simp [isZeroOrProbabilityMeasure_iff, hf]

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