inter_cons — Mathlib

English

Let a be an element and l1, l2 be lists. Then (a :: l1) ∩ l2 = if a ∈ l2 then a ∷ (l1 ∩ l2) else (l1 ∩ l2).

Русский

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

LaTeX

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

Lean4

@[grind =]
theorem inter_cons (l₁ : List α) : (a :: l₁) ∩ l₂ = if a ∈ l₂ then a :: l₁ ∩ l₂ else l₁ ∩ l₂ := by
  split_ifs <;> simp_all

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