conservative_congr — Mathlib

English

If two measures have the same almost everywhere structure, the conservative property is equivalent for a fixed map.

Русский

Если два распределения имеют одинаковую структуру почти везде, консервативность сохраняется между ними для фиксируемого отображения.

LaTeX

$$$\forall f,\mu,\nu:\ ae\,\mu = \ae\nu \Rightarrow (\mathrm{Conservative}(f,\mu) \iff \mathrm{Conservative}(f,\nu)).$$$

Lean4

theorem _root_.MeasureTheory.conservative_congr {ν : Measure α} (h : ae μ = ae ν) :
    Conservative f μ ↔ Conservative f ν :=
  ⟨(congr_ae · h), (congr_ae · h.symm)⟩

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