apply_mem_neighborSet_iff — Mathlib

English

Let f : G ↪g G' be a graph embedding. Then for all v,w ∈ V, f w ∈ G'.neighborSet (f v) iff w ∈ G.neighborSet v.

Русский

Пусть f : G ↪g G' — вложение графов. Тогда для любых вершин v,w ∈ V верно: f(w) сосед с f(v) в G' тогда и только тогда w сосед с v в G.

LaTeX

$$$ \forall v,w \in V,\ f w \in G'.neighborSet (f v) \iff w \in G.neighborSet v$$$

Lean4

theorem apply_mem_neighborSet_iff {v w : V} : f w ∈ G'.neighborSet (f v) ↔ w ∈ G.neighborSet v :=
  map_adj_iff f

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