coeSubgraph_adj — Mathlib

English

For G' : G.Subgraph, G'' : G'.coe.Subgraph and v,w ∈ V, the adjacency in G'.coeSubgraph G'' corresponds to adjacency in G'' lifted to the vertices with their verifications.

Русский

Для G' : G.Subgraph, G'' : G'.coe.Subgraph и вершин v,w ∈ V, смежность в G'.coeSubgraph G'' соответствует смежности в G'' для подлинных вершин и их встраиваний.

LaTeX

$$$(G'.\\mathrm{coeSubgraph} G'').\\mathrm{Adj}\ v\ w \\iff \\exists hv\\exists hw\\, G''.\\mathrm{Adj}\\langle v, hv\\rangle \\langle w, hw\\rangle$$$

Lean4

theorem coeSubgraph_adj {G' : G.Subgraph} (G'' : G'.coe.Subgraph) (v w : V) :
    (G'.coeSubgraph G'').Adj v w ↔ ∃ (hv : v ∈ G'.verts) (hw : w ∈ G'.verts), G''.Adj ⟨v, hv⟩ ⟨w, hw⟩ := by
  simp [Relation.Map]

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