toMeasure_zero — Mathlib

English

The outer measure toMeasure of 0 is 0 under a compatible measurability structure.

Русский

Внешняя мера toMeasure нуля равна нулю при допустимой структуре измеримости.

LaTeX

$$$$ \text{toMeasure}(0) = 0. $$$$

Lean4

@[simp]
theorem _root_.MeasureTheory.OuterMeasure.toMeasure_zero [ms : MeasurableSpace α]
    (h : ms ≤ (0 : OuterMeasure α).caratheodory) : (0 : OuterMeasure α).toMeasure h = 0 :=
  by
  ext s hs
  simp [hs]

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