English
Intersection of a set t with a biUnion equals the biUnion of intersections: t ∩ s.biUnion f = s.biUnion (λ x, t ∩ f x).
Русский
Пересечение множества t с biUnion равно biUnion пересечений: t ∩ s.biUnion f = s.biUnion (λ x, t ∩ f x).
LaTeX
$$$t \\cap s.biUnion f = s.biUnion (\\lambda x \\mapsto t \\cap f x)$$$
Lean4
theorem biUnion_inter (s : Finset α) (f : α → Finset β) (t : Finset β) : s.biUnion f ∩ t = s.biUnion fun x ↦ f x ∩ t :=
by grind