English
There is an equivalence between the cone point and the sections of F, given by sectionOfCone and the lift along the limit t.
Русский
Существует эквивалентность между точкой конуса и секциями F, заданная через sectionOfCone и ливер через предел t.
LaTeX
$$$\\text{isLimitEquivSections }(c)(t) : c.pt \\simeq F.sections,\\;\\text{toFun}=\\text{sectionOfCone } c,\\;\\text{invFun}=t.lift(\\mathrm{coneOfSection}( - ).2, \\langle \\rangle).$$$
Lean4
/-- The equivalence between a limiting cone of `F` in `Type u` and the "concrete" definition as the
sections of `F`. -/
noncomputable def isLimitEquivSections {c : Cone F} (t : IsLimit c) : c.pt ≃ F.sections
where
toFun := sectionOfCone c
invFun s := t.lift (coneOfSection s.2) ⟨⟩
left_inv x := (congr_fun (t.uniq (coneOfSection _) (fun _ ↦ x) fun _ ↦ rfl) ⟨⟩).symm
right_inv s := Subtype.ext (funext fun j ↦ congr_fun (t.fac (coneOfSection s.2) j) ⟨⟩)
