isCaratheodory_iff_le — Mathlib

English

MeasurableSet[OuterMeasure.caratheodory m] s iff for all t, m(t ∩ s) + m(t \ s) ≤ m t.

Русский

Измеримость множества s по Caratheodory эквивалентна неравенству для всех t: m(t ∩ s) + m(t \ s) ≤ m t.

LaTeX

$$MeasurableSet[OuterMeasure.caratheodory m] s ↔ ∀ t, m(t ∩ s) + m(t \ s) ≤ m t$$

Lean4

theorem isCaratheodory_iff_le {s : Set α} :
    MeasurableSet[OuterMeasure.caratheodory m] s ↔ ∀ t, m (t ∩ s) + m (t \ s) ≤ m t :=
  isCaratheodory_iff_le' m

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