sub_le_self

Mathlib.Data.Multiset.AddSub

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

English

s - t ≤ s.

Русский

s - t ≤ s.

LaTeX

$$$s - t \le s$$$

Lean4

protected theorem sub_le_self (s t : Multiset α) : s - t ≤ s :=
  by
  rw [Multiset.sub_le_iff_le_add]
  exact le_add_right _ _

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

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

Разделы

Аффилиация

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