preservesPullbackInr'

Mathlib.CategoryTheory.Extensive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr'

← MathLib Explorer

English

If C is small, then Discrete(C) is small.

Русский

Если C малая, то Discrete(C) малая.

LaTeX

$$$\text{Small}(C) \Rightarrow \text{Small}(\text{Discrete}(C))$$$

Lean4

noncomputable instance preservesPullbackInr' : PreservesLimit (cospan f coprod.inr) F :=
  by
  apply preservesLimit_of_iso_diagram (K₁ := cospan (f ≫ (coprod.braiding X Y).hom) coprod.inl)
  apply cospanExt (Iso.refl _) (Iso.refl _) (coprod.braiding X Y).symm <;> simp

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

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

Разделы

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

Аффилиация

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