whiskerRight_apply

Mathlib.CategoryTheory.Monoidal.Types.Basic

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

English

For a morphism f: Y → Z and X a type, the right whiskering by X yields (f ▷ X) p = (f p.1, p.2) for p ∈ Y ⊗ X.

Русский

Правый взмах по X даёт (f ∘) p = (f(p.1), p.2) для p ∈ Y ⊗ X.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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