verts_coeSubgraph — Mathlib

English

The vertex set of Subgraph.coeSubgraph G'' equals the underlying vertex set of G''.verts.

Русский

Множество вершин Subgraph.coeSubgraph G'' равно базовому множеству вершин G''.verts.

LaTeX

$$$(\\mathrm{Subgraph.coeSubgraph} G'').\\mathrm{verts} = (G''.\\mathrm{verts} : \\mathrm{Set} V)$$$

Lean4

@[simp]
theorem verts_coeSubgraph {G' : Subgraph G} (G'' : Subgraph G'.coe) :
    (Subgraph.coeSubgraph G'').verts = (G''.verts : Set V) :=
  rfl

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