bagInter_nil_iff_inter_nil — Mathlib

English

For all l1, l2, l1.bagInter l2 = [] iff l1 ∩ l2 = [].

Русский

Для всех l1, l2: l1.bagInter l2 = [] тогда и только тогда, когда l1 ∩ l2 = [].

LaTeX

$$$\\\\forall {\\\\alpha} [\\\\mathrm{DecidableEq} \\\\alpha] (l_1 l_2 : List \\\\alpha), l_1.bagInter l_2 = [] \\\\leftrightarrow l_1 \\\\cap l_2 = []$$$

Lean4

theorem bagInter_nil_iff_inter_nil : ∀ l₁ l₂ : List α, l₁.bagInter l₂ = [] ↔ l₁ ∩ l₂ = []
  | [], l₂ => by simp
  | b :: l₁, l₂ => by
    by_cases h : b ∈ l₂
    · simp [h]
    · simpa [h] using bagInter_nil_iff_inter_nil l₁ l₂

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