hasColimit_iff_small_colimitType — Mathlib

English

HasColimit F is equivalent to Small.(F ⋙ forget).ColimitType.

Русский

Существование колимита F эквивалентно тому, что Small.(F ⋙ forget).ColimitType малого размера.

LaTeX

$$$ \mathrm{HasColimit } F \iff \mathrm{Small}.(F \circ \mathrm{forget}).\mathrm{ColimitType} $$$

Lean4

theorem hasColimit_iff_small_colimitType : HasColimit F ↔ Small.{u} (F ⋙ forget).ColimitType :=
  by
  rw [← Types.hasColimit_iff_small_colimitType]
  constructor <;> intro
  · infer_instance
  · exact ⟨⟨_, isColimitCoconeOfForget _ (colimit.isColimit _)⟩⟩

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