comap_top — Mathlib

English

If f is injective, then the comap of the complete graph on W by f equals the complete graph on V: (completeGraph W).comap f = completeGraph V.

Русский

Если отображение f инъективно, то комап полного графа на W по f равен полному графу на V.

LaTeX

$$$$ (completeGraph W).comap f = completeGraph V $$$$

Lean4

theorem comap_top {f : V → W} (hf : f.Injective) : (completeGraph W).comap f = completeGraph V := by ext;
  simp [hf.eq_iff]

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