card_neighborSet_union_compl_neighborSet

English

If V is finite, the cardinality of the union equals |V| - 1.

Русский

Если множество вершин конечно, кардинал объединения равен |V| − 1.

LaTeX

$$$\\#\\big(G.neighborSet(v) \\cup G^{c}.neighborSet(v)\\big) = |V| - 1$$$

Lean4

theorem card_neighborSet_union_compl_neighborSet [Fintype V] (G : SimpleGraph V) (v : V)
    [Fintype (G.neighborSet v ∪ Gᶜ.neighborSet v : Set V)] :
    #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1 := by
  classical
    simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl, Finset.card_compl, Set.toFinset_card,
    Set.card_singleton]

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