toAffineLift_some — Mathlib

English

If P has homogeneous coordinates [X,Y,1], then the affine lift exists as a definite affine point: toAffineLift ⟨h⟩ = some affine point corresponding to (X,Y).

Русский

Если P имеет однородные координаты [X,Y,1], то восхождение к аффинной точке существует и соответствует некоей аффинной точке, связаннной с (X,Y).

LaTeX

$$$\\text{toAffineLift}(\\langle h \\rangle) = \\text{AffinePoint}\, (X,Y)$$$

Lean4

theorem toAffineLift_some {X Y : F} (h : W.NonsingularLift ⟦![X, Y, 1]⟧) :
    toAffineLift ⟨h⟩ = .some ((nonsingular_some ..).mp h) :=
  toAffine_some h

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