add_le_add_iff_right

Mathlib.Data.Multiset.AddSub

URI: https://scilib.ai/kg/mathlib#Multiset.add_le_add_iff_right

English

For multisets s, t, u, s + u ≤ t + u iff s ≤ t.

Русский

Для мультисетов s, t, u выполняется s + u ≤ t + u тогда и только тогда, когда s ≤ t.

LaTeX

$$$s + u \le t + u \iff s \le t$$$

Lean4

protected theorem add_le_add_iff_right : s + u ≤ t + u ↔ s ≤ t :=
  Quotient.inductionOn₃ s t u fun _ _ _ => subperm_append_right _

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

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

Разделы

Аффилиация

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