Theorems · Theorem · combinatorics

SimpleGraph.card_edgeFinset_bipartiteDoubleCover

∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj],
  G.bipartiteDoubleCover.edgeFinset.card = 2 * G.edgeFinset.card

The bipartite double cover of G has twice the number of edges as G.

Defined in: Mathlib.Combinatorics.SimpleGraph.Bipartite
Cited by: 1 results in Mathlib
Foundations: Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype DecidableRel

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Fintypestatement and proof · cited by 7,736
Finset.univproof · cited by 3,473
SimpleGraphstatement and proof · cited by 3,072
Finset.cardstatement and proof · cited by 2,327
SimpleGraph.Adjstatement and proof · cited by 1,346
Finset.filterproof · cited by 949
Sym2statement and proof · cited by 737
Sym2.mkproof · cited by 332
Finset.filter_congrproof · cited by 167
SimpleGraph.edgeFinsetstatement and proof · cited by 116
Sym2.indproof · cited by 66
SimpleGraph.Adj.symmproof · cited by 66

Cited by1

Results whose statement or proof uses this declaration.

SimpleGraph.two_mul_extremalNumber_le_zarankiewicz_symmproof · cited by 0