equation_neg — Mathlib

English

If two points on W share the same x and their y’s are not the negative of one another, then they have the same y-coordinate.

Русский

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

LaTeX

$$$W.Equation x_1 y_1 \rightarrow W.Equation x_2 y_2 \rightarrow (x_1 = x_2) \rightarrow (y_1 = y_2) \lor (y_1 = W.negY x_2 y_2)$$$

Lean4

theorem equation_neg (x y : R) : W'.Equation x (W'.negY x y) ↔ W'.Equation x y :=
  by
  rw [equation_iff, equation_iff, negY]
  congr! 1
  ring1

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