disjoint_cons_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem disjoint_cons_right {a : α} {s t : Multiset α} : Disjoint s (a ::ₘ t) ↔ a ∉ s ∧ Disjoint s t := by
  rw [_root_.disjoint_comm, disjoint_cons_left]; tauto

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