isLimit_types_iff — Mathlib

English

A multifork c in Type is a limit iff the map c.toSections: c.pt → I.sections is bijective.

Русский

Мультфорк c в категории типов является пределом тогда и только тогда, когда отображение c.toSections: c.pt → I.sections биективно.

LaTeX

$$$\\text{IsLimit}(c) \\iff \\text{Bijective}(c.toSections)$$$

Lean4

/-- A multifork `c : Multifork I` in the category of types is limit iff the
map `c.toSections : c.pt → I.sections` is a bijection. -/
theorem isLimit_types_iff : Nonempty (IsLimit c) ↔ Function.Bijective c.toSections := by
  rw [Types.isLimit_iff_bijective_sectionOfCone, ← toSections_fac, EquivLike.comp_bijective]

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