iff_of_arrow_iso_right — Mathlib

English

HasLiftingProperty is invariant under arrow Iso on the right.

Русский

Sвойство подъёма инвариантно относительно изоморфизма стрелки справа.

LaTeX

$$$$ HasLiftingProperty i p \\iff HasLiftingProperty i p' $$$$

Lean4

theorem iff_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') : HasLiftingProperty i p ↔ HasLiftingProperty i p' :=
  by
  constructor <;> intro
  exacts [of_arrow_iso_right i e, of_arrow_iso_right i e.symm]

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