measure_preimage_le — Mathlib

English

If f preserves μa to μb, then μa(f^{-1}(s)) ≤ μb(s) for all sets s.

Русский

Если f сохраняет μa→μb, то μa(f^{-1}(s)) ≤ μb(s) для любых множеств s.

LaTeX

$$$\text{MeasurePreserving } f\, μ_a\, μ_b \rightarrow \forall s, μ_a(f^{-1}(s)) \le μ_b(s)$$$

Lean4

theorem measure_preimage_le {f : α → β} (hf : MeasurePreserving f μa μb) (s : Set β) : μa (f ⁻¹' s) ≤ μb s :=
  by
  rw [← hf.map_eq]
  exact le_map_apply hf.aemeasurable _

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