le_add_right

Mathlib.MeasureTheory.Measure.MeasureSpace

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

English

μ1 ≤ μ2 iff ∀ S, μ1(S) ≤ μ2(S).

Русский

μ1 ≤ μ2 тогда и только тогда, когда ∀ S, μ1(S) ≤ μ2(S).

LaTeX

$$$ μ_1 \\le μ_2 \\iff \\forall S, μ_1(S) \\le μ_2(S) $$$

Lean4

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

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

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

Разделы

Аффилиация

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