iff_of_arrow_iso_left — Mathlib

English

HasLiftingProperty is invariant under arrow Iso on the left.

Русский

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

LaTeX

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

Lean4

theorem iff_of_arrow_iso_left {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'} (e : Arrow.mk i ≅ Arrow.mk i')
    (p : X ⟶ Y) : HasLiftingProperty i p ↔ HasLiftingProperty i' p :=
  by
  constructor <;> intro
  exacts [of_arrow_iso_left e p, of_arrow_iso_left e.symm p]

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