Theorems · Theorem · combinatorics

Rel.interedges_eq_biUnion

∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β}
  [inst_1 : DecidableEq α] [inst_2 : DecidableEq β],
  Rel.interedges r s t = s.biUnion fun x => Finset.map { toFun := fun x_1 => (x, x_1), inj' := ⋯ } ({y ∈ t | r x y})

Defined in

Mathlib.Combinatorics.SimpleGraph.Density

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidablePredDecidableEqDecidableEq