lanUnit_desc — Mathlib

English

For a HasLeftKanExtension f g and s ∈ LeftExtension f g, lanUnit f g composed with f whiskered lanDesc s equals s.unit.

Русский

Для HasLeftKanExtension f g и элемента s ∈ LeftExtension f g композиция lanUnit f g с f ◁ lanDesc s равна s.unit.

LaTeX

$$$\mathrm{lanUnit}(f,g) \;\circ\; (f \triangleleft \mathrm{lanDesc}(s)) = s.\mathrm{unit}$$$

Lean4

@[reassoc (attr := simp)]
theorem lanUnit_desc [HasLeftKanExtension f g] (s : LeftExtension f g) : lanUnit f g ≫ f ◁ lanDesc s = s.unit :=
  (lanIsKan f g).fac s

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