mem_bagInter — Mathlib

English

For any a, l1, l2, a ∈ l1.bagInter l2 iff a ∈ l1 ∧ a ∈ l2.

Русский

Для любого a, l1, l2 верно: a ∈ l1.bagInter l2 тогда и только тогда, когда a ∈ l1 и a ∈ l2.

LaTeX

$$$\\forall {\\\\alpha} [\\\\mathrm{DecidableEq} \\\\alpha] {a : \\\\alpha} {l_1 l_2 : List \\\\alpha}, a ∈ l_1.bagInter l_2 \\\\leftrightarrow a ∈ l_1 \\\\wedge a ∈ l_2$$$

Lean4

@[simp]
theorem mem_bagInter {a : α} {l₁ l₂ : List α} : a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂ := by
  fun_induction List.bagInter with grind

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