toOuterMeasure_caratheodory — Mathlib

English

The outer measure defined by a PMF is Carathéodory-measurable on every set; i.e., it is a top outer measure.

Русский

Пусть p — PMF. Тогда p.toOuterMeasure является карматеодорической на любом множестве; т.е. это полная внешняя мера.

LaTeX

$$$ p.toOuterMeasure.caratheodory = \top $$$

Lean4

@[simp]
theorem toOuterMeasure_caratheodory : p.toOuterMeasure.caratheodory = ⊤ :=
  by
  refine eq_top_iff.2 <| le_trans (le_sInf fun x hx => ?_) (le_sum_caratheodory _)
  have ⟨y, hy⟩ := hx
  exact ((le_of_eq (dirac_caratheodory y).symm).trans (le_smul_caratheodory _ _)).trans (le_of_eq hy)

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