isCaratheodory_iff_le' — Mathlib

English

Carathéodory measurability is equivalent to the subadditivity inequality m(t ∩ s) + m(t \\ s) ≤ m(t) for all t.

Русский

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

LaTeX

$$$IsCaratheodory(m)(s) \\\\iff \\\\forall t, m(t\\\\cap s) + m(t\\\\setminus s) \\\\le m t$$$

Lean4

theorem isCaratheodory_iff_le' {s : Set α} : IsCaratheodory m s ↔ ∀ t, m (t ∩ s) + m (t \ s) ≤ m t :=
  forall_congr' fun _ => le_antisymm_iff.trans <| and_iff_right <| measure_le_inter_add_diff _ _ _

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