ndinsert_le — Mathlib

English

ndinsert a s ≤ t iff s ≤ t and a ∈ t.

Русский

ndinsert a s ≤ t эквивалентно s ≤ t и a ∈ t.

LaTeX

$$$ ndinsert\\ a\\ s \\le t \\iff (s \\le t) \\land a \\in t $$$

Lean4

theorem ndinsert_le {a : α} {s t : Multiset α} : ndinsert a s ≤ t ↔ s ≤ t ∧ a ∈ t :=
  ⟨fun h => ⟨le_trans (le_ndinsert_self _ _) h, mem_of_le h (mem_ndinsert_self _ _)⟩, fun ⟨l, m⟩ =>
    if h : a ∈ s then by simp [h, l]
    else by
      rw [ndinsert_of_notMem h, ← cons_erase m, cons_le_cons_iff, ← le_cons_of_notMem h, cons_erase m]
      exact l⟩

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