conservative — Mathlib

English

If f preserves a finite measure μ, then f is conservative with respect to μ.

Русский

Если отображение f сохраняет конечную меру μ, то оно консервативно относительно μ.

LaTeX

$$$[\text{IsFiniteMeasure }\mu]\ wedge \mathrm{MeasurePreserving}(f,\mu,\mu)\Rightarrow \mathrm{Conservative}(f,\mu).$$$

Lean4

/-- A self-map preserving a finite measure is conservative. -/
protected theorem conservative [IsFiniteMeasure μ] (h : MeasurePreserving f μ μ) : Conservative f μ :=
  ⟨h.quasiMeasurePreserving, fun _ hsm h0 => h.exists_mem_iterate_mem hsm.nullMeasurableSet h0⟩

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