card_edgeFinset_le_card_choose_two

English

Any graph on n vertices has at most n choose 2 edges.

Русский

Любой граф на n вершинах имеет не более n выбрать 2 рёбер.

LaTeX

$$$ #G.edgeFinset \le (Fintype.card V).choose 2 $$$

Lean4

/-- Any graph on `n` vertices has at most `n.choose 2` edges. -/
theorem card_edgeFinset_le_card_choose_two : #G.edgeFinset ≤ (Fintype.card V).choose 2 := by
  classical
  rw [← card_edgeFinset_top_eq_card_choose_two]
  exact card_le_card (edgeFinset_mono le_top)

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