two_mul_card_edgeFinset — Mathlib

English

The number of ordered vertex pairs (x,y) with x adjacent to y is twice the number of edges.

Русский

Число упорядоченных пар вершин $(x,y)$ с соседством равно удвоенному числу рёбер.

LaTeX

$$$2 \cdot \#G.edgeFinset = \#\{(x,y) \in V \times V \mid G.Adj x y\}$$$

Lean4

theorem two_mul_card_edgeFinset : 2 * #G.edgeFinset = #(univ.filter fun (x, y) ↦ G.Adj x y) :=
  by
  rw [← dart_card_eq_twice_card_edges, ← card_univ]
  refine card_bij' (fun d _ ↦ (d.fst, d.snd)) (fun xy h ↦ ⟨xy, (mem_filter.1 h).2⟩) ?_ ?_ ?_ ?_ <;> simp

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