map — Mathlib

English

Let G be a simple graph. If G is LocallyLinear, then its relabeled version under any vertex embedding f remains LocallyLinear.

Русский

Пусть G — простой граф. Если G обладает свойством локальной линейности, то граф после переназначения вершин через отображение f остаётся с тем же свойством.

LaTeX

$$$\\forall f:\\alpha\\hookrightarrow\\beta\\;\\forall G:\\text{SimpleGraph }\\alpha,\\; G\\text{ LocallyLinear } \\Rightarrow (G.map\\ f)\\text{ LocallyLinear }$$$

Lean4

theorem map (f : α ↪ β) (hG : G.LocallyLinear) : (G.map f).LocallyLinear :=
  by
  refine ⟨hG.1.map _, ?_⟩
  rintro _ _ ⟨a, b, h, rfl, rfl⟩
  obtain ⟨s, hs, ha, hb⟩ := hG.2 h
  exact ⟨s.map f, hs.map, mem_map_of_mem _ ha, mem_map_of_mem _ hb⟩

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