inter_cons_of_mem — Mathlib

English

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

Русский

Пусть a — элемент, а l1, l2 — списки. Если a ∈ l2, тогда (a :: l1) ∩ l2 = a :: (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 = a :: l_1 \\\\cap l_2$$$

Lean4

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

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