instSmallFullSubcategoryOfSmall

Mathlib.CategoryTheory.ObjectProperty.Small

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

Lean4

instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] : Small.{w} P.FullSubcategory :=
  small_of_surjective (f := fun (x : Subtype P) ↦ ⟨x.1, x.2⟩) (fun x ↦ ⟨⟨x.1, x.2⟩, rfl⟩)

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

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

Разделы

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

Аффилиация

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