hasLimit_iff_small_sections — Mathlib

English

For a diagram F : J ⥤ Type, F has a limit if and only if F.sections is small.

Русский

Для диаграммы F : J ⥤ Type существование предела эквивалентно тому, что F.sections является малой (small).

LaTeX

$$$\\text{HasLimit } F \\iff \\text{Small}(F.\\mathrm{sections})$$$

Lean4

theorem hasLimit_iff_small_sections (F : J ⥤ Type u) : HasLimit F ↔ Small.{u} F.sections :=
  ⟨fun _ =>
    .mk ⟨_, ⟨(Equiv.ofBijective _ ((isLimit_iff_bijective_sectionOfCone (limit.cone F)).mp ⟨limit.isLimit _⟩)).symm⟩⟩,
    fun _ => ⟨_, Small.limitConeIsLimit F⟩⟩
    -- TODO: If `UnivLE` works out well, we will eventually want to deprecate these
    -- definitions, and probably as a first step put them in namespace or otherwise rename them.

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