measure_union_le

Mathlib.MeasureTheory.OuterMeasure.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measure_union_le

English

For sets s,t, μ(s ∪ t) ≤ μ s + μ t.

Русский

Для множеств s,t верно μ(s ∪ t) ≤ μ(s) + μ(t).

LaTeX

$$$\; μ(s \cup t) \le μ(s) + μ(t)$$$

Lean4

theorem measure_union_le (s t : Set α) : μ (s ∪ t) ≤ μ s + μ t := by
  simpa [union_eq_iUnion] using measure_iUnion_fintype_le μ (cond · s t)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru