mem_ndunion — Mathlib

English

For multisets s and t and element a, a belongs to the ndunion of s and t if and only if a belongs to s or a belongs to t.

Русский

Для мультимножества s и t и элемента a: a принадлежит ndunion(s,t) тогда и только тогда, когда a принадлежит s или a принадлежит t.

LaTeX

$$$a \\in \\mathrm{ndunion}(s,t) \\iff a \\in s \\lor a \\in t$$$

Lean4

@[simp]
theorem mem_ndunion {s t : Multiset α} {a : α} : a ∈ ndunion s t ↔ a ∈ s ∨ a ∈ t :=
  Quot.induction_on₂ s t fun _ _ => List.mem_union_iff

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