negInduction

Mathlib.Data.Int.Init

URI: https://scilib.ai/kg/mathlib#Int.negInduction

Lean4

/-- Inductively define a function on `ℤ` by defining it on `ℕ` and extending it from `n` to `-n`. -/
@[elab_as_elim]
protected def negInduction {motive : ℤ → Sort*} (nat : ∀ n : ℕ, motive n)
    (neg : (∀ n : ℕ, motive n) → ∀ n : ℕ, motive (-n)) : ∀ n : ℤ, motive n
  | .ofNat n => nat n
  | .negSucc n => neg nat <| n + 1

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru