comap_injective — Mathlib

English

If f: X→Y is surjective, then precomposition comap f is injective on LocallyConstant maps: if comap f g = comap f h, then g = h.

Русский

Если f сюръективно отображает X на Y, то предобраз comap f инъективен на локально константных отображениях: если comap f g = comap f h, тогда g = h.

LaTeX

$$$ (\\text{comap } f).\\mathrm{Injective} \\quad\\text{assuming } f \\text{ surjective}$$$

Lean4

theorem comap_injective (f : C(X, Y)) (hfs : f.1.Surjective) : (comap (Z := Z) f).Injective :=
  by
  intro a b h
  ext y
  obtain ⟨x, hx⟩ := hfs y
  simpa [← hx] using LocallyConstant.congr_fun h x

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