comap_map — Mathlib

English

If f is injective, comap followed by map along f is the original matroid: (N.comap f).map f hf = N.

Русский

Если f инъективно, то применение comap, затем map вдоль f возвращает исходный матроид: (N.comap f).map f hf = N.

LaTeX

$$$ (N.comap\ f).map f hf = N $$$

Lean4

theorem comap_map {f : α → β} (hf : f.Injective) : (M.map f hf.injOn).comap f = M := by
  simp [ext_iff_indep, preimage_image_eq _ hf, and_iff_left hf.injOn, image_eq_image hf]

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