map_comap_le — Mathlib

English

Let f be an embedding f: V ↪ W and G a simple graph on W. Then the graph obtained by pulling back G along f to V and then pushing forward along f is contained in G.

Русский

Пусть f: V ↪ W является вложением, и G — простой граф на W. Тогда граф, полученный путем вытягивания обратно графа G по f на V, а затем его отображения по f, содержится в G.

LaTeX

$$$ (\\mathrm{map}\\ f\\ (\\mathrm{comap}\\ f\\ G)) \\le G $$$

Lean4

theorem map_comap_le (f : V ↪ W) (G : SimpleGraph W) : (G.comap f).map f ≤ G := by rw [map_le_iff_le_comap]

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