support_map — Mathlib

English

For an embedding f: V ↪ W, the support of the mapped graph equals the image of the support of the original graph: (G.map f).support = f '' G.support.

Русский

Для вложения f: V ↪ W множество вершин графа после отображения равно образу множества вершин исходного графа: (G.map f).support = f '' G.support.

LaTeX

$$$$ (G.map f).\\text{support} = f'' G.\\text{support}. $$$$

Lean4

theorem support_map (f : V ↪ W) (G : SimpleGraph V) : (G.map f).support = f '' G.support := by ext; simp [mem_support];
  tauto

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