Y_eq_of_Y_ne — Mathlib

English

If two points on W have the same x-coordinate, then their y-coordinates are either equal or one is the negation of the other with respect to x.

Русский

Если две точки кривой W имеют одинаковую абсциссу, то их ординаты либо совпадают, либо одна равна противоположной другой по отношению к x.

LaTeX

$$$(h_1 : W.Equation x_1 y_1) \rightarrow (h_2 : W.Equation x_2 y_2) \rightarrow hx : x_1 = x_2 \rightarrow (y_1 = y_2 \lor y_1 = W.negY x_2 y_2)$$$

Lean4

theorem Y_eq_of_Y_ne {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hx : x₁ = x₂)
    (hy : y₁ ≠ W.negY x₂ y₂) : y₁ = y₂ :=
  (Y_eq_of_X_eq h₁ h₂ hx).resolve_right hy

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