inter_cons_of_notMem — Mathlib

English

Let a be an element and l1, l2 be lists. If a ∉ l2, then (a :: l1) ∩ l2 = l1 ∩ l2.

Русский

Пусть a — элемент, а l1, l2 — списки. Если a ∉ l2, тогда (a :: l1) ∩ l2 = l1 ∩ l2.

LaTeX

$$$\\forall {\\\\alpha} [\\\\mathrm{DecidableEq} \\\\alpha] (l_1 : List \\\\alpha) (a : \\\\alpha) (l_2 : List \\\\alpha) (h : a ∉ l_2), (a :: l_1) \\\\cap l_2 = l_1 \\\\cap l_2$$$

Lean4

@[simp]
theorem inter_cons_of_notMem (l₁ : List α) (h : a ∉ l₂) : (a :: l₁) ∩ l₂ = l₁ ∩ l₂ := by
  simp [Inter.inter, List.inter, h]

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