sub_le_iff_le_add — Mathlib

English

For multisets s,t,u of α, s - t ≤ u if and only if s ≤ u + t.

Русский

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

LaTeX

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

Lean4

/-- This is a special case of `tsub_le_iff_right`, which should be used instead of this.
This is needed to prove `OrderedSub (Multiset α)`. -/
protected theorem sub_le_iff_le_add : s - t ≤ u ↔ s ≤ u + t := by
  induction t using Multiset.induction_on generalizing s with
  | empty => simp [Multiset.sub_zero]
  | cons a s IH => simp [IH, erase_le_iff_le_cons]

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