inter_biUnion — Mathlib

English

Same as the previous, but with the arguments ordered differently: t ∩ s.biUnion f = s.biUnion (λ x, t ∩ f x).

Русский

То же самое, но с другой постановкой: 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 inter_biUnion (t : Finset β) (s : Finset α) (f : α → Finset β) : t ∩ s.biUnion f = s.biUnion fun x ↦ t ∩ f x :=
  by grind

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