adj — Mathlib

English

Let G be a simple graph and let G' be an induced subgraph of G. Then for all a,b in the vertex set of G', a is adjacent to b in G' if and only if a is adjacent to b in G.

Русский

Пусть G — простой граф, и G' — индуцированный подграф G. Тогда для любых вершин a,b из вершин G' верно: a смежна с b в G' тогда и только тогда, когда a смежна с b в G.

LaTeX

$$$\\forall G\\;\\forall H\\subseteq G\\; (H\\text{ induces } G) \\Rightarrow \\forall a,b \\in V(H),\\ H.Adj(a,b) \\iff G.Adj(a,b)$$$

Lean4

@[simp]
protected theorem adj {G' : G.Subgraph} (hG' : G'.IsInduced) {a b : G'.verts} : G'.Adj a b ↔ G.Adj a b :=
  ⟨coe_adj_sub _ _ _, hG' a.2 b.2⟩

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