zero_sub

Mathlib.Data.Multiset.AddSub

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

English

s - t ≤ u ↔ s ≤ u + t

Русский

s - t ≤ u эквивалентно s ≤ u + t.

LaTeX

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

Lean4

protected theorem zero_sub (t : Multiset α) : 0 - t = 0 :=
  Multiset.induction_on t rfl fun a s ih => by simp [ih]

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

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

Разделы

Аффилиация

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