card_edgeFinset_completeEquipartiteGraph

English

The total number of edges in K_r(t) is C(r,2)·t^2.

Русский

Общее число ребер в K_r(t) равно комбинаторному числу C(r,2) умноженному на t^2.

LaTeX

$$edgeFinset.card = \binom{r}{2} \cdot t^{2}$$

Lean4

theorem card_edgeFinset_completeEquipartiteGraph : #(completeEquipartiteGraph r t).edgeFinset = r.choose 2 * t ^ 2 :=
  by
  rw [← mul_right_inj' two_ne_zero, ← sum_degrees_eq_twice_card_edges]
  conv_lhs =>
    rhs; intro v
    rw [degree_completeEquipartiteGraph v]
  rw [sum_const, smul_eq_mul, card_univ, card_prod, Fintype.card_fin, Fintype.card_fin]
  conv_rhs => rw [← Nat.mul_assoc, Nat.choose_two_right, Nat.mul_div_cancel' r.even_mul_pred_self.two_dvd]
  rw [← mul_assoc, mul_comm r _, mul_assoc t _ _, mul_comm t, mul_assoc _ t, ← pow_two]

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