instSmallPair

Mathlib.CategoryTheory.ObjectProperty.Small

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.instSmallPair

English

For any objects X, Y, the pair (X, Y) is small as an object-property.

Русский

Для любых объектов X, Y пара (X, Y) является малым свойством объектов.

LaTeX

$$ (X Y : C) → (\text{pair } X Y).Small$$

Lean4

instance (X Y : C) : ObjectProperty.Small.{w} (.pair X Y) :=
  by
  dsimp [pair]
  infer_instance

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

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

Разделы

Аффилиация

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