existsUnique — Mathlib

English

Let HasLeftKanLift f g. Then for s ∈ LeftLift f g, there exists a unique τ with lanLiftUnit f g ≫ τ ▷ f = s.unit.

Русский

Пусть HasLeftKanLift f g. Тогда для s ∈ LeftLift f g существует единственный τ такой, что lanLiftUnit f g ≫ τ ▷ f = s.unit.

LaTeX

$$$\exists! \tau,\; \mathrm{lanLiftUnit}(f,g) \;\circ\; (\tau \; \text{whiskered by } f) = s.\mathrm{unit}$$$

Lean4

theorem existsUnique [HasLeftKanLift f g] (s : LeftLift f g) : ∃! τ, lanLiftUnit f g ≫ τ ▷ f = s.unit :=
  (lanLiftIsKan f g).existsUnique _

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