limitCone_pt_ext — Mathlib

English

If two elements of the limit cone have the same coordinates under the projection maps, then they are equal.

Русский

Если два элемента лимитного конуса имеют одинаковые координаты через проекции, то они равны.

LaTeX

$$$\\text{limitCone_pt_ext}:\\forall x,y:\\,(\\text{limitCone } F).pt,\\ (\\forall j, \\pi_j(x)=\\pi_j(y))\\Rightarrow x=y$$$

Lean4

@[ext]
theorem limitCone_pt_ext {x y : (limitCone F).pt}
    (w : (equivShrink F.sections).symm x = (equivShrink F.sections).symm y) : x = y := by simp_all

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