Theorems · Theorem · combinatorics
SimpleGraph.encard_edgeSet_completeBipartiteGraph
∀ {W₁ : Type u_2} {W₂ : Type u_3}, (completeBipartiteGraph W₁ W₂).edgeSet.encard = ENat.card W₁ * ENat.card W₂- Cited by
- 1 results in Mathlib
- Foundations
- Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- ENatstatement and proof · cited by 4,985
- Set.rangeproof · cited by 4,705
- Set.univproof · cited by 3,945
- Sym2statement and proof · cited by 737
- Sym2.mkproof · cited by 332
- Set.encardstatement and proof · cited by 327
- Set.image_univproof · cited by 322
- SimpleGraph.edgeSetstatement · cited by 199
- ENat.cardstatement and proof · cited by 89
- completeBipartiteGraphstatement · cited by 16
- Set.encard_univproof · cited by 15
Cited by1
Results whose statement or proof uses this declaration.
- SimpleGraph.IsBipartiteWith.encard_edgeSet_leproof · cited by 1