whiskerLeft_apply

Mathlib.CategoryTheory.Monoidal.Types.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.whiskerLeft_apply

English

For a morphism f: Y → Z and X a type, the left whiskering by X sends p ∈ X ⊗ Y to (p.1, f p.2).

Русский

Левый взмах по X отправляет элемент p ∈ X ⊗ Y в (p.1, f(p.2)).

LaTeX

$$$(X \\triangleleft f) p = (p.1, f(p.2)).$$$

Lean4

@[simp]
theorem whiskerLeft_apply (X : Type u) {Y Z : Type u} (f : Y ⟶ Z) (p : X ⊗ Y) : (X ◁ f) p = (p.1, f p.2) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru