cons_bagInteger — Mathlib

English

For any a, l1, l2, bagInter (cons a l1) l2 equals if a ∈ l2 then a :: (l1.bagInter (l2.erase a)) else (l1.bagInter l2).

Русский

Для любого a, l1, l2 bagInter (cons a l1) l2 равняется if a ∈ l2 then a :: (l1.bagInter (l2.erase a)) иначе l1.bagInter l2.

LaTeX

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

Lean4

@[grind =]
theorem cons_bagInteger : (a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂ := by
  split_ifs <;> simp_all

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