instCommuteWith_1 — Mathlib

English

If f,g are such that HasLeftKanLift f g and h: x ⟶ c, then LanLift.CommuteWith f g h holds, giving HasLeftKanLift f (h ≫ g).

Русский

Если f,g удовлетворяют условиям HasLeftKanLift f g и h: x ⟶ c, то LanLift.CommuteWith f g h выполняется и получается HasLeftKanLift f (h ≫ g).

LaTeX

$$$[HasLeftKanLift f g] \Rightarrow [LanLift.CommuteWith f g h] \Rightarrow [HasLeftKanLift f (h \gg g)].$$$

Lean4

instance [HasAbsLeftKanLift f g] {x : B} (h : x ⟶ c) : LanLift.CommuteWith f g h :=
  HasAbsLeftKanLift.commute h

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