cons_bagInter_of_pos — Mathlib

English

If a ∈ l2, then (a :: l1).bagInter l2 = a :: l1.bagInter (l2.erase a).

Русский

Если a ∈ l2, то (a :: l1).bagInter l2 = a :: l1.bagInter (l2.erase a).

LaTeX

$$$\\forall {\\\\alpha} {l_2 : List \\\\alpha} {a : \\\\alpha} [\\\\mathrm{DecidableEq} \\\\alpha] (l_1 : List \\\\alpha), a ∈ l_2 → (List.\\\\cons a l_1).bagInter l_2 = List.\\\\cons a (l_1.bagInter (l_2.erase a))$$$

Lean4

@[simp]
theorem cons_bagInter_of_pos (l₁ : List α) (h : a ∈ l₂) : (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a) := by
  cases l₂ with grind [List.bagInter]

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