small_of_small_arrow

Mathlib.CategoryTheory.Comma.CardinalArrow

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

← MathLib Explorer

English

If Arrow C is small, then C is small.

Русский

Если Arrow C малая, то C малая.

LaTeX

$$$\\\\operatorname{Small}(C) \\\\Leftarrow \\\\operatorname{Small}(\\\\operatorname{Arrow}(C))$$$

Lean4

theorem small_of_small_arrow (C : Type u) [Category.{v} C] [Small.{w} (Arrow C)] : Small.{w} C :=
  small_of_injective (f := fun X ↦ Arrow.mk (𝟙 X)) (fun _ _ h ↦ congr_arg Comma.left h)

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

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

Разделы

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

Аффилиация

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