biUnion_inter — Mathlib

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

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