limitEquivSections — Mathlib

English

In the Small setting, equality of limit cone elements is determined by equality of their Shrink-coordinates.

Русский

В малом случае равенство элементов предельного конуса определяется равенством их Shrink-координат.

LaTeX

$$$\\text{limitCone_pt_ext} : \\forall x,y,\\ (\\mathrm{equivShrink} F.sections).symm x = (\\mathrm{equivShrink} F.sections).symm y \\Rightarrow x=y$$$

Lean4

/-- The equivalence between the abstract limit of `F` in `Type max v u`
and the "concrete" definition as the sections of `F`.
-/
noncomputable def limitEquivSections : limit F ≃ F.sections :=
  isLimitEquivSections (limit.isLimit F)

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