disjoint_ndinsert_right — Mathlib

English

Let α be a type with decidable equality. For any a ∈ α and multisets s and t, Disjoint s (ndinsert a t) holds iff a ∉ s and Disjoint s t.

Русский

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

LaTeX

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

Lean4

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

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