injective_range_liftQ_of_exact — Mathlib

English

If h is exact, then the map ((range f).liftQ g h) is injective.

Русский

Если h — точность, тогда отображение ((range f).liftQ g h) инъективно.

LaTeX

$$$$ \\operatorname{Injective}((\\operatorname{range} f).liftQ g (h .|>\\mathrm{mpr})). $$$$

Lean4

theorem injective_range_liftQ_of_exact (h : Function.Exact f g) : Function.Injective ((range f).liftQ g (h · |>.mpr)) :=
  by simpa only [← LinearMap.ker_eq_bot, ker_eq_bot_range_liftQ_iff, exact_iff] using h

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