Theorems · Definition · order theory

SuccAddOrder.casesOn

{α : Type u_1} →
  [inst : Preorder α] →
    [inst_1 : Add α] →
      [inst_2 : One α] →
        {motive : SuccAddOrder α → Sort u} →
          (t : SuccAddOrder α) →
            ([toSuccOrder : SuccOrder α] →
                (succ_eq_add_one : ∀ (x : α), SuccOrder.succ x = x + 1) →
                  motive { toSuccOrder := toSuccOrder, succ_eq_add_one := succ_eq_add_one }) →
              motive t

Defined in

Mathlib.Algebra.Order.SuccPred

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

PreorderAddOne