hasLiftingProperty_of_wfs — Mathlib

English

If for all arrows i and p with hi: W1 i and hp: W2 p there is a lifting property, then HasLiftingProperty i p holds for any such i,p.

Русский

Если для любых стрелок i и p с hi: W1 i и hp: W2 p существует подъем, то HasLiftingProperty i p выполняется для любых таких i,p.

LaTeX

$$$ \forall {A,B,X,Y} (i:A\to B) (p:X\to Y), W_1 i \to W_2 p \to HasLiftingProperty i p $$$

Lean4

theorem hasLiftingProperty_of_wfs {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) (hi : W₁ i) (hp : W₂ p) :
    HasLiftingProperty i p :=
  (llp_eq_of_wfs W₁ W₂ ▸ hi) p hp

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