fac — Mathlib

English

For an IsKan t and s in LeftExtension f g, the equality t.unit ≫ f ◁ desc s = s.unit holds.

Русский

Для t, являющегося IsKan, и элемента s в LeftExtension f g, выполняется тождество t.unit ≫ f ◁ desc s = s.unit.

LaTeX

$$$\operatorname{fac} (\mathsf{IsKan}\, t)\; s: \; t.unit \circ (f \triangleleft (\mathsf{desc}\, s)) = s.\mathrm{unit}$$$

Lean4

@[reassoc (attr := simp)]
theorem fac (H : IsKan t) (s : LeftExtension f g) : t.unit ≫ f ◁ H.desc s = s.unit :=
  StructuredArrow.IsUniversal.fac H s

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