apply_mem_neighborSet — Mathlib

English

The image of a dart under a graph homomorphism is obtained by applying f to the endpoints and mapping the adjacency accordingly.

Русский

Образ стрелы (dart) под графом-гомоморфизмом получается путем применения f к концам и соответствующего отображения смежности.

LaTeX

$$$ f.\\mathrm{mapDart}(d) = \\langle d.1.map\\ f\\ f,\\ f.\\mathrm{map\\_adj}(d.2) \\rangle $$$

Lean4

theorem apply_mem_neighborSet {v w : V} (h : w ∈ G.neighborSet v) : f w ∈ G'.neighborSet (f v) :=
  map_adj f h

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