hasLimits — Mathlib

English

The category of profinite spaces has all small limits; equivalently, every small diagram of profinite spaces has a limit.

Русский

Категория профинидальных пространств имеет все малые пределы; эквивалентно, всякая малая диаграмма из профинидальных пространств имеет предел.

LaTeX

$$$\\forall J\\,[\\text{SmallCategory }J],\\ \\forall F:\\ J\\to\\mathrm{Profinite},\\ \\exists L\\ \\text{ such that } L \\text{ is the limit of }F\\text{ in Profinite with projection maps }(\\pi_j: L\\to F(j)).$$$

Lean4

instance hasLimits : Limits.HasLimits Profinite :=
  hasLimits_of_hasLimits_createsLimits Profinite.toTopCat

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