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