le_caratheodory — Mathlib

English

If μ is metric outer measure, then borel X ≤ μ.caratheodory, i.e. all Borel sets are Carathéodory-measurable within μ.

Русский

Если μ — метрическая внешняя мера, то борелевское множество X менее чем μ.caratéodory, т.е. борелевские множества измеримы по μ.

LaTeX

$$borel X ≤ μ.caratheodory$$

Lean4

theorem le_caratheodory [MeasurableSpace X] [BorelSpace X] (hm : IsMetric μ) : ‹MeasurableSpace X› ≤ μ.caratheodory :=
  by
  rw [BorelSpace.measurable_eq (α := X)]
  exact hm.borel_le_caratheodory

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