hasLimit_iff_small_sections — Mathlib

English

HasLimit F holds if and only if the family of sections of the forgetful functor along F is small.

Русский

Существование предела HasLimit F эквивалентно тому, что множество секцийAlong F через забывающий функтор малого размера.

LaTeX

$$$ \text{HasLimit } F \;\Longleftrightarrow\; \operatorname{Small}\,(F \circ \mathrm{forget}).\mathrm{sections} $$$

Lean4

theorem hasLimit_iff_small_sections : HasLimit F ↔ Small.{u} ((F ⋙ forget).sections) :=
  by
  rw [← Types.hasLimit_iff_small_sections]
  constructor <;> intro
  · infer_instance
  · exact ⟨⟨_, isLimitConeOfForget _ (limit.isLimit _)⟩⟩

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