x_pos — Mathlib

English

If x>0 and y>0 for a solution a, then for any positive integer exponent n, (a^n).y > 0.

Русский

Если x>0 и y>0 для решения a, то для любого положительного целого n, (a^n).y > 0.

LaTeX

$$$\forall a\in \mathrm{Solution}_1(d),\; a_x>0 \land a_y>0 \rightarrow \forall n\in \mathbb{Z}_{>0},\; (a^n)_y > 0$$$

Lean4

/-- A fundamental solution has positive `x`. -/
theorem x_pos {a : Solution₁ d} (h : IsFundamental a) : 0 < a.x :=
  zero_lt_one.trans h.1

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