card_edgeFinset_top_eq_card_choose_two

English

For a graph on n vertices, the complete graph on n vertices has exactly n choose 2 edges.

Русский

Для графа на n вершин полный граф имеет ровно n выбрать 2 рёбер.

LaTeX

$$$ #(\top : SimpleGraph V).edgeFinset = (Fintype.card V).choose 2 $$$

Lean4

/-- The complete graph on `n` vertices has `n.choose 2` edges. -/
theorem card_edgeFinset_top_eq_card_choose_two [DecidableEq V] :
    #(⊤ : SimpleGraph V).edgeFinset = (Fintype.card V).choose 2 := by
  simp_rw [Set.toFinset_card, edgeSet_top, Set.coe_setOf, ← Sym2.card_subtype_not_diag]

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