piLT — Mathlib

English

If i is a limit point in a well-ordered indexing, then piLT X i is isomorphic to the limit over all j<i of piLTProj maps.

Русский

Если i—предел в хорошо упорядоченном индексационном наборе, то piLT X i изоморфен предельному пределу по всем j<i через piLTProj.

LaTeX

$$$\\piLT X i \\cong\\mathrm{limit}\\; (\\mathrm{piLTProj}\\; i)$$$

Lean4

/-- For a family of types `X` indexed by an preorder `ι` and an element `i : ι`,
`piLT X i` is the product of all the types indexed by elements below `i`. -/
abbrev piLT (X : ι → Type*) (i : ι) :=
  ∀ l : Iio i, X l

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