card_verts — Mathlib

English

For a spanning subgraph, the number of vertices equals the number of vertices of the whole graph.

Русский

Для растягивающего подграфа число вершин равно числу вершин всего графа.

LaTeX

$$$\forall G' : G.Subgraph\,\text{IsSpanning} : G'.verts.toFinset.card = |V|$$$

Lean4

theorem card_verts [Fintype V] {G' : Subgraph G} [Fintype G'.verts] (h : G'.IsSpanning) :
    G'.verts.toFinset.card = Fintype.card V :=
  by
  simp only [isSpanning_iff.1 h, Set.toFinset_univ]
  congr

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