finset_card_neighborSet_eq_degree

English

The Finset version of neighborSet cardinality equals the degree.

Русский

Кардинал множества соседей в виде Finset равен степени.

LaTeX

$$$\forall {G' : Subgraph G} {v}, [Fintype (G'.neighborSet v).Elem] : (G'.neighborSet v).toFinset.card = G'.degree v$$$

Lean4

theorem finset_card_neighborSet_eq_degree {G' : Subgraph G} {v : V} [Fintype (G'.neighborSet v)] :
    (G'.neighborSet v).toFinset.card = G'.degree v := by rw [degree, Set.toFinset_card]

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