mapDart_apply — Mathlib

English

The image of a dart under a graph homomorphism is a pair consisting of the mapped endpoint and the mapped adjacency.

Русский

Образ стрелы графа под гомоморфизмом — это пара, состоящая из образа конца и образа смежности.

LaTeX

$$$ f.mapDart d = \\langle d.1.map f f, f.map_adj d.2 \\rangle $$$

Lean4

@[simp]
theorem mapDart_apply (d : G.Dart) : f.mapDart d = ⟨d.1.map f f, f.map_adj d.2⟩ :=
  rfl

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