le_add_left

Mathlib.MeasureTheory.Measure.MeasureSpace

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

English

If μ ≤ ν then μ ≤ ν + ν'.

Русский

Если μ ≤ ν, то μ ≤ ν + ν'.

LaTeX

$$$ \\text{If } μ \\le ν \\text{ then } μ \\le ν + ν' $$$

Lean4

protected theorem le_add_left (h : μ ≤ ν) : μ ≤ ν' + ν := fun s => le_add_left (h s)

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

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

Разделы

Аффилиация

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