Theorems · Theorem · order theory

Succ.rec

∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {m : α} {P : (n : α) → m ≤ n → Prop},
  P m ⋯ → (∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯) → ∀ ⦃n : α⦄ (hmn : m ≤ n), P n hmn

Induction principle on a type with a SuccOrder for all elements above a given element m.

Defined in

Mathlib.Order.SuccPred.Archimedean

Cited by

10 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Quot.sound

Assumes

PreorderSuccOrderIsSuccArchimedean