Theorems · Theorem · combinatorics

SimpleGraph.interedges_biUnion

∀ {ι : Type u_2} {κ : Type u_3} {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq α]
  (s : Finset ι) (t : Finset κ) (f : ι → Finset α) (g : κ → Finset α),
  G.interedges (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab => G.interedges (f ab.1) (g ab.2)

Defined in

Mathlib.Combinatorics.SimpleGraph.Density

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableRelDecidableEq