coe_degree — Mathlib

English

The coe-degree of a vertex matches the degree in the subgraph.

Русский

Степень в подграфе через коэр совпадает со степенью.

LaTeX

$$$G'.\mathrm{coe}.degree v = G'.\mathrm{degree} v$$$

Lean4

@[simp]
theorem coe_degree (G' : Subgraph G) (v : G'.verts) [Fintype (G'.coe.neighborSet v)] [Fintype (G'.neighborSet v)] :
    G'.coe.degree v = G'.degree v := by
  rw [← card_neighborSet_eq_degree]
  exact Fintype.card_congr (coeNeighborSetEquiv v)

Похожие утверждения