IsFundamental — Mathlib

English

If a.x > 0, then for every natural n, (a^n).x > 0.

Русский

Если a.x > 0, то для каждого натурального n выполняется (a^n).x > 0.

LaTeX

$$$\forall a\in \mathrm{Solution}_1(d),\; a_x>0 \rightarrow \forall n\in \mathbb{N},\; (a^n)_x > 0$$$

Lean4

/-- We define a solution to be *fundamental* if it has `x > 1` and `y > 0`
and its `x` is the smallest possible among solutions with `x > 1`. -/
def IsFundamental (a : Solution₁ d) : Prop :=
  1 < a.x ∧ 0 < a.y ∧ ∀ {b : Solution₁ d}, 1 < b.x → a.x ≤ b.x

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