nonneg_cases — Mathlib

English

If a ∈ Z√d is nonnegative, there exist x,y ∈ N such that a equals ⟨x,y⟩ or ⟨x,-y⟩ or ⟨-x,y⟩.

Русский

Если $a\\in \\mathbb{Z}[\\sqrt{d}]$ неотрицателен, существуют $x,y\\in \\mathbb{N}$ такие, что $a = \\langle x,y\\rangle$ или $a=\\langle x,-y\\rangle$ или $a=\\langle -x,y\\rangle$.

LaTeX

$$∃ x,y ∈ ℕ, a = ⟨x,y⟩ ∨ a = ⟨x,-y⟩ ∨ a = ⟨-x,y⟩$$

Lean4

theorem nonneg_cases : ∀ {a : ℤ√d}, Nonneg a → ∃ x y : ℕ, a = ⟨x, y⟩ ∨ a = ⟨x, -y⟩ ∨ a = ⟨-x, y⟩
  | ⟨(x : ℕ), (y : ℕ)⟩, _ => ⟨x, y, Or.inl rfl⟩
  | ⟨(x : ℕ), -[y+1]⟩, _ => ⟨x, y + 1, Or.inr <| Or.inl rfl⟩
  | ⟨-[x+1], (y : ℕ)⟩, _ => ⟨x + 1, y, Or.inr <| Or.inr rfl⟩
  | ⟨-[_+1], -[_+1]⟩, h => False.elim h

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