nonnegg_cases_right — Mathlib

English

For c,d and a ∈ ℤ, if for all natural x we have x = -x implies SqLe x c a d, then Nonnegg c d a b holds for all b ∈ ℤ.

Русский

Для c,d и a ∈ ℤ, если ∀ x ∈ ℕ, b = -x ⇒ SqLe x c a d, тогда Nonnegg c d a b для всех b ∈ ℤ.

LaTeX

$$$\forall b: \mathbb{Z}, \ (\forall x \in \mathbb{N}, b = -x \Rightarrow \mathrm{SqLe}(x,c,a,d)) \Rightarrow \mathrm{Nonnegg}(c,d)(a,b)$$$

Lean4

theorem nonnegg_cases_right {c d} {a : ℕ} : ∀ {b : ℤ}, (∀ x : ℕ, b = -x → SqLe x c a d) → Nonnegg c d a b
  | (b : Nat), _ => trivial
  | -[b+1], h => h (b + 1) rfl

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