degree_eq_card_sub_part_card — Mathlib

English

The degree of a vertex equals the size of the complement of its adjacency relative to the vertex set, i.e. |V| minus the size of its non-neighborhood part.

Русский

Степень вершины равна размеру множества вершин, не смежных с данной вершиной, в терминах разбиения.

LaTeX

$$$G.\deg(s) = |V| - |\{t : \neg G.Adj(s,t)\}| = |V| - (h.finpartition.part s).card.$$$

Lean4

theorem degree_eq_card_sub_part_card [DecidableEq V] : G.degree s = Fintype.card V - #(h.finpartition.part s) :=
  calc
    _ = #{t | G.Adj s t} := by simp [← card_neighborFinset_eq_degree, neighborFinset]
    _ = Fintype.card V - #{t | ¬G.Adj s t} := (eq_tsub_of_add_eq (filter_card_add_filter_neg_card_eq_card _))
    _ = _ := by
      congr; ext; rw [mem_filter]
      convert Finpartition.mem_part_ofSetoid_iff_rel.symm
      simp [setoid]

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