instZero — Mathlib

English

If μ and ν agree on all measurable atoms, then μ = ν.

Русский

Если две меры совпадают на всех измеримых атомах, то они равны.

LaTeX

$$$$ \forall x,\ μ(\text{measurableAtom}(x)) = ν(\text{measurableAtom}(x)) \Rightarrow μ = ν. $$$$

Lean4

instance instZero {_ : MeasurableSpace α} : Zero (Measure α) :=
  ⟨{  toOuterMeasure := 0
      m_iUnion := fun _f _hf _hd => tsum_zero.symm
      trim_le := OuterMeasure.trim_zero.le }⟩

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