of_arrow_iso_right — Mathlib

English

Preservation of lifting under right-arrow iso in the Arrow category.

Русский

Сохранение подъёма при правой стрелке-изоморфизме в категории стрелок.

LaTeX

$$$$ HasLiftingProperty\\big( Arrow.mk i \\big)\\; p \\Rightarrow HasLiftingProperty\\big( Arrow.mk i' \\big)\\; p $$$$

Lean4

theorem of_arrow_iso_right {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'} (e : Arrow.mk p ≅ Arrow.mk p')
    [hip : HasLiftingProperty i p] : HasLiftingProperty i p' :=
  by
  rw [Arrow.iso_w' e]
  infer_instance

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