English
A recursive decomposition: disjiUnion (cons a s ha) f H can be expressed in terms of disjiUnion of singleton a and of s, with a compatible disjointness condition.
Русский
Рекурсивное разложение: disjiUnion (cons a s ha) f H разбивается на disjiUnion от одиночного элемента a и от s с условием дизjointности.
LaTeX
$$$ disjiUnion (cons a s ha) f H = (f a).disjUnion (s.disjiUnion f) (\\lambda _ hb _ hc \\mapsto H (mem_cons_of_mem hb) (mem_cons_of_mem hc)) \\\\ \\ \\ \\ (disjoint_left.2 \\dots ) $$$
Lean4
@[simp]
theorem disjiUnion_cons (a : α) (s : Finset α) (ha : a ∉ s) (f : α → Finset β) (H) :
disjiUnion (cons a s ha) f H =
(f a).disjUnion ((s.disjiUnion f) fun _ hb _ hc ↦ H (mem_cons_of_mem hb) (mem_cons_of_mem hc))
(disjoint_left.2 fun _ hb h ↦
let ⟨_, hc, h⟩ := mem_disjiUnion.mp h
disjoint_left.mp (H (mem_cons_self a s) (mem_cons_of_mem hc) (ne_of_mem_of_not_mem hc ha).symm) hb h) :=
eq_of_veq <| Multiset.cons_bind _ _ _
