cons_bagInter_of_neg — Mathlib

English

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

Русский

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

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 = l_1.bagInter l_2$$$

Lean4

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

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