Theorems · Definition · combinatorics
SimpleGraph.Subgraph.degree
{V : Type u} → {G : SimpleGraph V} → (G' : G.Subgraph) → (v : V) → [Fintype ↑(G'.neighborSet v)] → ℕThe degree of a vertex in a subgraph. It's zero for vertices outside the subgraph.
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- Assumes
- Fintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Set.Elemstatement and proof · cited by 7,166
- SimpleGraphstatement and proof · cited by 3,072
- Fintype.cardproof · cited by 1,386
- SimpleGraph.Subgraphstatement and proof · cited by 326
- SimpleGraph.Subgraph.neighborSetstatement and proof · cited by 46
Cited by14
Results whose statement or proof uses this declaration.
- SimpleGraph.Subgraph.coe_degreestatement and proof · cited by 3
- SimpleGraph.Subgraph.degree_eq_zero_of_subsingletonstatement · cited by 2
- SimpleGraph.Subgraph.isMatching_iff_forall_degreestatement · cited by 1
- SimpleGraph.Subgraph.finset_card_neighborSet_eq_degreestatement · cited by 1
- SimpleGraph.Subgraph.degree_of_notMem_vertsstatement · cited by 1
- SimpleGraph.Subgraph.isPerfectMatching_iff_forall_degreestatement · cited by 0
- SimpleGraph.Subgraph.degree_eq_one_iff_existsUnique_adjstatement · cited by 0
- SimpleGraph.Subgraph.degree_lestatement and proof · cited by 0
- SimpleGraph.Subgraph.degree_le'statement · cited by 0
- SimpleGraph.Subgraph.degree_pos_iff_exists_adjstatement · cited by 0
- SimpleGraph.Subgraph.degree_spanningCoestatement and proof · cited by 0
- SimpleGraph.Subgraph.nontrivial_verts_of_degree_ne_zerostatement and proof · cited by 0