Theorems · Theorem · combinatorics

SimpleGraph.degree_toSubgraph

∀ {V : Type u} (G H : SimpleGraph V) (h : H ≤ G) {v : V} [inst : Fintype ↑((SimpleGraph.toSubgraph H h).neighborSet v)]
  [inst_1 : Fintype ↑(H.neighborSet v)], (SimpleGraph.toSubgraph H h).degree v = H.degree v

Defined in

Mathlib.Combinatorics.SimpleGraph.Subgraph

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeFintype