instSmallUnopOfOpposite

Mathlib.CategoryTheory.ObjectProperty.Small

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

← MathLib Explorer

English

If P is small, then its unop is small: P.unop.Small.

Русский

Если P мал, то P.unop мал.

LaTeX

$$P.Small ⇒ P.unop.Small$$

Lean4

instance (P : ObjectProperty Cᵒᵖ) [ObjectProperty.Small.{w} P] : ObjectProperty.Small.{w} P.unop := by
  simpa only [← small_congr P.unop.subtypeOpEquiv]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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