Theorems · Theorem · combinatorics

SimpleGraph.degree_le_of_le

∀ {V : Type u_1} {G : SimpleGraph V} {v : V} [inst : Fintype ↑(G.neighborSet v)] {H : SimpleGraph V}
  [inst_1 : Fintype ↑(H.neighborSet v)], G ≤ H → G.degree v ≤ H.degree v

If G ≤ H then G.degree v ≤ H.degree v for any vertex v.

Defined in

Mathlib.Combinatorics.SimpleGraph.Finite

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeFintype