edgeSet_univ_card — Mathlib

English

Let G be a finite simple graph on vertex set V. Then the number of edges counted from the edge set equals the number of elements in the edgeFinset, i.e., the edgeFinset enumerates all edges.

Русский

Пусть G — конечный простой граф на множестве вершин V. Тогда число рёбер, считанных из множества рёбер, равно числу элементов в edgeFinset; то есть edgeFinset перечисляет все рёбра.

LaTeX

$$$ #(univ : Finset G.edgeSet) = #G.edgeFinset $$$

Lean4

@[simp]
theorem edgeSet_univ_card : #(univ : Finset G.edgeSet) = #G.edgeFinset :=
  Fintype.card_of_subtype G.edgeFinset fun _ => mem_edgeFinset

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