le_sum_caratheodory — Mathlib

English

The infimum of Carathéodory structures is less than or equal to the Carathéodory of the sum.

Русский

Наименьшее из Caratheodory(m_i) не больше Caratheodory(∑ m_i).

LaTeX

$$⨅ i, (m i).caratheodory ≤ (sum m).caratheodory$$

Lean4

theorem le_sum_caratheodory {ι} (m : ι → OuterMeasure α) : ⨅ i, (m i).caratheodory ≤ (sum m).caratheodory :=
  fun s h t => by simp [fun i => MeasurableSpace.measurableSet_iInf.1 h i t, ENNReal.tsum_add]

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