equivProjectivization_symm_apply_mk

English

The inverse of the equivalence sends a projective point [x:y] to ∞ if y = 0, otherwise to x/y.

Русский

Обратное отображение превращает точку [x:y] в ∞, если y=0, иначе в x/y.

LaTeX

$$$(\\equivProjectivization(K))^{-1}([x:y])=\\begin{cases} \\infty, & y=0 \\\\ x/y, & y\\neq 0 \\end{cases}$$$

Lean4

@[simp]
theorem equivProjectivization_symm_apply_mk (x y : K) (h : (x, y) ≠ 0) :
    (equivProjectivization K).symm (mk K ⟨x, y⟩ h) = if y = 0 then ∞ else y⁻¹ * x := by simp [equivProjectivization]

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