limitSemiring — Mathlib

English

Construction of a limit cone in SemiRingCat: the cone point is the underlying type of the limit cone in Types.Small, with projections defined via the chosen limit homomorphisms.

Русский

Построение предельного конуса в SemiRingCat: вершина конуса — это базовый тип предельного конуса в Types.Small, проекции задаются через выбранные гомоморфизмы предела.

LaTeX

$$$\mathrm{limitCone} \colon \text{Cone } F$$$

Lean4

instance limitSemiring : Semiring (Types.Small.limitCone.{v, u} (F ⋙ forget SemiRingCat.{u})).pt :=
  let _ : Semiring (F ⋙ forget SemiRingCat).sections := (sectionsSubsemiring F).toSemiring
  inferInstanceAs <| Semiring (Shrink (F ⋙ forget SemiRingCat).sections)

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