add_le_add_iff_left

Mathlib.Data.Multiset.AddSub

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

English

For multisets s, t, u, the order relation satisfies s + t ≤ s + u iff t ≤ u.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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