product_biUnion — Mathlib

English

The biUnion over f of the product equals the product of the biUnion: (s ×ˢ t).biUnion f = s.biUnion (λ a, t.biUnion (λ b, f(a,b))).

Русский

Объединение по функции f над произведением равно произведению объединений: (s ×ˢ t).biUnion f = s.biUnion(λ a, t.biUnion(λ b, f(a,b))).

LaTeX

$$$(s \timesˢ t).biUnion f = s.biUnion \bigl( \lambda a: t.biUnion (\lambda b: f(a,b)) \bigr)$$$

Lean4

/-- See also `Finset.sup_product_left`. -/
@[simp]
theorem product_biUnion [DecidableEq γ] (s : Finset α) (t : Finset β) (f : α × β → Finset γ) :
    (s ×ˢ t).biUnion f = s.biUnion fun a => t.biUnion fun b => f (a, b) := by grind

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