disjoint_cons_left — Mathlib

English

Let a be an element and s,t multisets. Then Disjoint (a ::ₘ s) t holds iff a ∉ t and Disjoint s t.

Русский

Пусть a — элемент, а s, t — мультисеты. Тогда Disjoint (a ::ₘ s) t эквивалентно a ∉ t и Disjoint s t.

LaTeX

$$$Disjoint (a ::ₘ s) t \\iff a \\notin t \\land Disjoint s t$$$

Lean4

@[simp]
theorem disjoint_cons_left {a : α} {s t : Multiset α} : Disjoint (a ::ₘ s) t ↔ a ∉ t ∧ Disjoint s t :=
  (@disjoint_add_left _ { a } s t).trans <| by rw [singleton_disjoint]

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