preimage_null

Mathlib.Dynamics.Ergodic.MeasurePreserving

URI: https://scilib.ai/kg/mathlib#MeasureTheory.MeasurePreserving.preimage_null

← MathLib Explorer

English

If f preserves μa to μb and μb(s) = 0, then μa(f^{-1}(s)) = 0.

Русский

Если f сохраняет μa→μb и μb(s)=0, то μa(f^{-1}(s))=0.

LaTeX

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

Lean4

theorem preimage_null {f : α → β} (hf : MeasurePreserving f μa μb) {s : Set β} (hs : μb s = 0) : μa (f ⁻¹' s) = 0 :=
  hf.quasiMeasurePreserving.preimage_null hs

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru