boundedBy_caratheodory — Mathlib

English

If hs holds for all t, then the Carathéodory σ-algebra of boundedBy m is measurable on s.

Русский

Если для всех t верно hs, то множество s карatheodory-измеримо относительно boundedBy m.

LaTeX

$$MeasurableSet[(boundedBy m).caratheodory] s$$

Lean4

theorem boundedBy_caratheodory {m : Set α → ℝ≥0∞} {s : Set α} (hs : ∀ t, m (t ∩ s) + m (t \ s) ≤ m t) :
    MeasurableSet[(boundedBy m).caratheodory] s :=
  by
  apply ofFunction_caratheodory; intro t
  rcases t.eq_empty_or_nonempty with h | h
  · simp [h, Set.not_nonempty_empty]
  · convert le_trans _ (hs t)
    · simp [h]
    exact add_le_add iSup_const_le iSup_const_le

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