Theorems · Theorem · combinatorics
SimpleGraph.Copy.degree_le
∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G.Copy H) (v : V)
[inst : Fintype ↑(G.neighborSet v)] [inst_1 : Fintype ↑(H.neighborSet (f v))], G.degree v ≤ H.degree (f v)- Defined in
- Mathlib.Combinatorics.SimpleGraph.Copy
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Fintypestatement and proof · cited by 7,736
- Set.Elemstatement and proof · cited by 7,166
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.neighborSetstatement and proof · cited by 257
- SimpleGraph.degreestatement · cited by 112
- Function.Embedding.injectiveproof · cited by 111
- SimpleGraph.Copystatement and proof · cited by 49
- Fintype.card_le_of_injectiveproof · cited by 19
- SimpleGraph.card_neighborSet_eq_degreeproof · cited by 9
- SimpleGraph.Copy.mapNeighborSetproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- SimpleGraph.Copy.minDegree_monoproof · cited by 2