disjoint_ndinsert_left — Mathlib

English

Let α be a type with decidable equality. For any a ∈ α and multisets s and t, the condition Disjoint (ndinsert a s) t is equivalent to a ∉ t and Disjoint s t.

Русский

Пусть α — множество с разрешимой эквивалентностью по равенству. Пусть a ∈ α и мультимножества s, t. Тогда несовместность Disjoint (ndinsert a s) t эквивалентна a ∉ t и Disjoint s t.

LaTeX

$$$\\mathrm{Disjoint}(\\mathrm{ndinsert}(a,s),t) \\iff a \\notin t \\land \\mathrm{Disjoint}(s,t)$$$

Lean4

@[simp]
theorem disjoint_ndinsert_left {a : α} {s t : Multiset α} : Disjoint (ndinsert a s) t ↔ a ∉ t ∧ Disjoint s t :=
  Iff.trans (by simp [disjoint_left]) disjoint_cons_left

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