theorem SimpleGraph.card_edgeFinset_completeGraph (V : Type u_1) [Fintype V] [DecidableEq V] : (completeGraph V).edgeFinset.card = (Fintype.card V).choose 2

The number of edges of the complete graph on a finite vertex type V is #V choose 2.

This is a thin completeGraph-flavoured restatement of Mathlib's SimpleGraph.card_edgeFinset_top_eq_card_choose_two, useful when a downstream definition is stated using the completeGraph V abbreviation rather than the ⊤ form. (Because completeGraph V reduces to ⊤, the two are definitionally equal.)

theorem SimpleGraph.card_edgeFinset_completeGraph_fin (n : ℕ) : (completeGraph (Fin n)).edgeFinset.card = n.choose 2

Specialisation of card_edgeFinset_completeGraph to Fin n.