Mathlib Map

Theorems · Definition · order theory

SuccOrder.succ

{α : Type u_3} → {inst : Preorder α} → [self : SuccOrder α] → α → α

Successor function

Defined in
Mathlib.Order.SuccPred.Basic
Cited by
13 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
SuccOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Order.succ · cited by 633Order.succOrdinalApprox.exists_lfpApprox_eq_lfpApprox · cited by 2OrdinalApprox.exists_lfpA…SuccAddOrder.succ_eq_add_one · cited by 1SuccAddOrder.succ_eq_add_…SuccOrder.ext · cited by 1SuccOrder.extSuccOrder.forall_ne_bot_iff · cited by 1SuccOrder.forall_ne_bot_i…SuccOrder.le_succ · cited by 1SuccOrder.le_succSuccOrder.max_of_succ_le · cited by 1SuccOrder.max_of_succ_leCardinal.not_injective_limitation_set · cited by 1Cardinal.not_injective_li…SuccOrder.succ_le_of_lt · cited by 1SuccOrder.succ_le_of_ltENat.succ_natCast · cited by 1ENat.succ_natCastENat.succ_top · cited by 0ENat.succ_topSuccAddOrder.noConfusion · cited by 0SuccAddOrder.noConfusionSuccAddOrder.noConfusionType · cited by 0SuccAddOrder.noConfusionT…SuccAddOrder.mk.noConfusion · cited by 0mk.noConfusionSuccAddOrder.recOn · cited by 0SuccAddOrder.recOnPreorder · cited by 7952PreorderSuccOrder · cited by 574SuccOrderSuccOrder.succCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Preorderstatement and proof · cited by 7,952
  • SuccOrderstatement and proof · cited by 574

Cited by20

Results whose statement or proof uses this declaration.