sub_le

Mathlib.MeasureTheory.Measure.Sub

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.sub_le

English

For measures μ, ν and d, μ - ν ≤ μ.

Русский

Для мер μ, ν и d верно μ - ν ≤ μ.

LaTeX

$$$\\\\mu - \\\\nu \\\\le \\\\mu$$$

Lean4

theorem sub_le : μ - ν ≤ μ :=
  sub_le_of_le_add <| Measure.le_add_right le_rfl

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

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

Разделы

Аффилиация

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