verts_spanningCoe_injective — Mathlib

English

The map G' ↦ (verts(G'), spanningCoe(G')) from Subgraph G into pairs is injective.

Русский

Отображение G' ↦ (verts(G'), spanningCoe(G')) от подграфов G в пары вершин и spanningCoe инъективно.

LaTeX

$$$ \\text{Injective}\\, (G' \\mapsto (\\mathrm{verts}(G'), \\mathrm{spanningCoe}(G'))) $$$

Lean4

theorem verts_spanningCoe_injective : (fun G' : Subgraph G => (G'.verts, G'.spanningCoe)).Injective :=
  by
  intro G₁ G₂ h
  rw [Prod.ext_iff] at h
  exact Subgraph.ext h.1 (spanningCoe_inj.1 h.2)

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