Theorems · Theorem · order theory

Succ.rec_bot

∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α] [IsSuccArchimedean α] (p : α → Prop),
  p ⊥ → (∀ (a : α), p a → p (Order.succ a)) → ∀ (a : α), p a

Defined in

Mathlib.Order.SuccPred.Archimedean

Cited by

1 results in Mathlib

Foundations

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

Assumes

PreorderOrderBotSuccOrderIsSuccArchimedean