sfinite

Mathlib.Dynamics.Ergodic.MeasurePreserving

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

English

If f preserves μa to μb and μa is σ-finite, then μb is σ-finite.

Русский

Если f сохраняет μa в μb и μa σ-конечна, то μb σ-конечна.

LaTeX

$$$\text{MeasurePreserving } f\, μ_a\, μ_b \rightarrow [SFinite\, μ_a] \rightarrow SFinite\, μ_b$$$

Lean4

protected theorem sfinite {f : α → β} (hf : MeasurePreserving f μa μb) [SFinite μa] : SFinite μb :=
  by
  rw [← hf.map_eq]
  infer_instance

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

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

Разделы

Аффилиация

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