English
The underlying multiset of disjiUnion s t is the bind of s with the underlying multisets of t; i.e., its first projection equals s.1.bind (λ a, (t a).1).
Русский
Основанная на множестве структура disjiUnion имеет вид s.1.bind (λ a, (t a).1).
LaTeX
$$$ (s.disjiUnion t h).1 = s.1.bind (fun a \\rightarrow (t a).1)$$$
Lean4
@[simp]
theorem disjiUnion_val (s : Finset α) (t : α → Finset β) (h) : (s.disjiUnion t h).1 = s.1.bind fun a ↦ (t a).1 :=
rfl