erase_le_iff_le_cons — Mathlib

English

s.erase a ≤ t iff s ≤ a ::ₘ t.

Русский

s.erase a ≤ t эквивалентно s ≤ a ::ₘ t.

LaTeX

$$$s\erase a \le t \iff s \le a ::ₘ t$$$

Lean4

theorem erase_le_iff_le_cons {s t : Multiset α} {a : α} : s.erase a ≤ t ↔ s ≤ a ::ₘ t :=
  ⟨fun h => le_trans (le_cons_erase _ _) (cons_le_cons _ h), fun h =>
    if m : a ∈ s then by rw [← cons_erase m] at h; exact (cons_le_cons_iff _).1 h
    else le_trans (erase_le _ _) ((le_cons_of_notMem m).1 h)⟩

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