id — Mathlib · SciLib

English

The identity map is conservative with respect to any measure μ.

Русский

Идентичное отображение conserve относительно любой меры μ.

LaTeX

$$$\mathrm{Conservative}(\mathrm{id},\mu).$$$

Lean4

/-- The identity map is conservative w.r.t. any measure. -/
protected theorem id (μ : Measure α) : Conservative id μ :=
  { toQuasiMeasurePreserving := QuasiMeasurePreserving.id μ
    exists_mem_iterate_mem' := fun _ _ h0 => by simpa [exists_ne] using nonempty_of_measure_ne_zero h0 }

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