hasAbsLeftKanLift — Mathlib

English

If HasAbsLeftKanLift f g, then LanLift.CommuteWith f g h holds for any h: x ⟶ c.

Русский

Если HasAbsLeftKanLift f g, то LanLift.CommuteWith f g h выполняется для любого h: x ⟶ c.

LaTeX

$$$[HasAbsLeftKanLift f g] \Rightarrow [LanLift.CommuteWith f g h].$$$

Lean4

theorem hasAbsLeftKanLift {t : LeftLift f g} (H : IsAbsKan t) : HasAbsLeftKanLift f g :=
  have : HasLeftKanLift f g := H.isKan.hasLeftKanLift
  ⟨fun h ↦ ⟨⟨H.ofIsoAbsKan (IsKan.uniqueUpToIso H.isKan (lanLiftIsKan f g)) h⟩⟩⟩

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