instSmallOfObjOfSmall

Mathlib.CategoryTheory.ObjectProperty.Small

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

← MathLib Explorer

English

If X : ι → C and ι is small, then (CategoryTheory.ObjectProperty.ofObj X).Small.

Русский

Если X : ι → C и ι мал, тогда (ofObj X).Small.

LaTeX

$$([Small.{w} ι]) → (ObjectProperty.ofObj X).Small$$

Lean4

instance {ι : Type*} (X : ι → C) [Small.{w} ι] : ObjectProperty.Small.{w} (ofObj X) :=
  small_of_surjective (f := fun i ↦ ⟨X i, by simp⟩) (by rintro ⟨_, ⟨i⟩⟩; simp)

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

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

Разделы

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

Аффилиация

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