sub_le_sub_right

Mathlib.Data.Multiset.AddSub

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

English

If s ≤ t, then s − u ≤ t − u.

Русский

Если s ⊆ t, то s − u ⊆ t − u.

LaTeX

$$$$ s \le t \Rightarrow s - u \le t - u $$$$

Lean4

protected theorem sub_le_sub_right (hst : s ≤ t) : s - u ≤ t - u :=
  Multiset.sub_le_iff_le_add'.mpr <| hst.trans Multiset.le_add_sub

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

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

Разделы

Аффилиация

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