instOuterMeasureClass — Mathlib

English

There is a canonical outer measure class structure on OuterMeasure α that records the basic properties (empty measure, monotonicity, and iUnion behavior).

Русский

Существует каноническая структура класса внешних мер на OuterMeasure α, фиксирующая базовые свойства: нуль на пустом множестве, монотонность и поведение на iUnion.

LaTeX

$$$\\text{OuterMeasureClass}(\\mathrm{OuterMeasure}\\; \\alpha)\\; \\alpha$$$

Lean4

instance : OuterMeasureClass (OuterMeasure α) α
    where
  measure_empty f := f.empty
  measure_mono f := f.mono
  measure_iUnion_nat_le f := f.iUnion_nat

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