English
If i is a limit in a linear order, then piLTLim establishes an equivalence between piLT X i and the limit of piLTProj maps.
Русский
Если i — предел в линейном порядке, то piLTLim даёт эквивленцию между piLT X i и пределом piLTProj.
LaTeX
$$$\\mathrm{piLTLim}\\; hi : \\mathrm{piLT}X i \\simeq \\mathrm{limit}\\; (\\mathrm{piLTProj}\\; i).Elem$$$
Lean4
/-- If `i` is a limit in a well-ordered type indexing a family of types,
then `piLT X i` is the limit of all `piLT X j` for `j < i`. -/
@[simps apply]
noncomputable def piLTLim : piLT X i ≃ limit (piLTProj (X := X)) i
where
toFun f := ⟨fun j ↦ piLTProj j.2.le f, fun _ _ _ ↦ rfl⟩
invFun f
l :=
let k := hi.mid l.2;
f.1 ⟨k, k.2.2⟩ ⟨l, k.2.1⟩
right_inv
f := by
ext j l
set k := hi.mid (l.2.trans j.2)
obtain le | le := le_total j ⟨k, k.2.2⟩
exacts [congr_fun (f.2 le) l, (congr_fun (f.2 le) ⟨l, _⟩).symm]
