coeSubgraph — Mathlib

English

An edge between v,w exists in G'.coe.Subgraph G'' iff there exist hv, hw with v,hv ∈ G'.verts, w,hw ∈ G'.verts and G''.Adj ⟨v,hv⟩ ⟨w,hw⟩.

Русский

Смежность между v и w в G'.coe.Subgraph G'' эквивалентна существованию hv, hw such that v ∈ G'.verts, w ∈ G'.verts и G''.Adj ⟨v,hv⟩ ⟨w,hw⟩.

LaTeX

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

Lean4

/-- Given a subgraph of a subgraph of `G`, construct a subgraph of `G`. -/
protected abbrev coeSubgraph {G' : G.Subgraph} : G'.coe.Subgraph → G.Subgraph :=
  Subgraph.map G'.hom

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