measure_le_measure_union_right

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

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

English

μ t ≤ μ (s ∪ t).

Русский

μ(t) ≤ μ(s ∪ t).

LaTeX

$$$\mu t \le \mu (s \cup t)$$$

Lean4

@[simp, mono]
theorem measure_le_measure_union_right : μ t ≤ μ (s ∪ t) :=
  μ.mono subset_union_right

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

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

Разделы

Аффилиация

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