instOuterMeasureClass — Mathlib

English

There is a canonical outer measure class structure on measures.

Русский

Существует каноническая структура класса внешней меры для мер.

LaTeX

$$Theorem instOuterMeasureClass (α) : OuterMeasureClass (Measure α) α$$

Lean4

instance instOuterMeasureClass [MeasurableSpace α] : OuterMeasureClass (Measure α) α
    where
  measure_empty m := measure_empty (μ := m.toOuterMeasure)
  measure_iUnion_nat_le m := m.iUnion_nat
  measure_mono m := m.mono

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