whiskeringLeft_comp_evaluation — Mathlib

English

Whiskering by F and then evaluating at a yields evaluation at F.obj a: (whiskeringLeft A B C).obj F ⋙ (evaluation A C).obj a = (evaluation B C).obj (F.obj a).

Русский

Склейка по левой части на F и последующая оценка в a дают оценку в F(a).

LaTeX

$$$(\\mathrm{whiskeringLeft}\\ A\\ B\\ C).\\mathrm{obj} F \\; \\circ (\\mathrm{evaluation}\\ A C).\\mathrm{obj} a = (\\mathrm{evaluation}\\ B C).\\mathrm{obj}(F.\\mathrm{obj} a)$$$

Lean4

/-- Whiskering by `F` and then evaluating at `a` is the same as evaluating at `F.obj a`. -/
@[simp]
theorem whiskeringLeft_comp_evaluation (F : A ⥤ B) (a : A) :
    (whiskeringLeft A B C).obj F ⋙ (evaluation A C).obj a = (evaluation B C).obj (F.obj a) :=
  rfl

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