nonnegg_cases_left — Mathlib

English

For c,d and b ∈ ℕ, a ∈ ℤ, if ∀ x ∈ ℕ, a = -x → SqLe x d b c, then Nonnegg c d a b holds.

Русский

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

LaTeX

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

Lean4

theorem nonnegg_cases_left {c d} {b : ℕ} {a : ℤ} (h : ∀ x : ℕ, a = -x → SqLe x d b c) : Nonnegg c d a b :=
  cast nonnegg_comm (nonnegg_cases_right h)

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