map_zero — Mathlib

English

Let f be any function. The pushforward of the zero measure by f is the zero measure: (0 : Measure α).map f = 0.

Русский

Пусть f произвольна. Образ нулевой меры по f равен нулевой мере: (0 : Measure α).map f = 0.

LaTeX

$$$ (0 : \mathrm{Measure}(\alpha)).map f = 0 $$$

Lean4

@[simp]
protected theorem map_zero (f : α → β) : (0 : Measure α).map f = 0 := by
  by_cases hf : AEMeasurable f (0 : Measure α) <;> simp [map, hf]

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