Theorems · Theorem · combinatorics

Rel.interedges_biUnion

∀ {ι : Type u_2} {κ : Type u_3} {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)]
  [inst_1 : DecidableEq α] [inst_2 : DecidableEq β] (s : Finset ι) (t : Finset κ) (f : ι → Finset α) (g : κ → Finset β),
  Rel.interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab => Rel.interedges r (f ab.1) (g ab.2)

Defined in

Mathlib.Combinatorics.SimpleGraph.Density

Cited by

1 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidablePredDecidableEqDecidableEq