SuccOrder

📁 Source: Mathlib/Order/Interval/Set/SuccOrder.lean

Statistics

Metric	Count
Definitions SuccOrder	1
Theorems coe_pred_of_not_isMin, pred_eq_of_not_isMin, coe_succ_of_not_isMax, succ_eq_of_not_isMax	4
Total	5

Set.Ici

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pred_of_not_isMin 📖	mathematical	IsMin Set.Elem Set.Ici PartialOrder.toPreorder Preorder.toLE Set Set.instMembership	Order.pred Subtype.preorder Set.OrdConnected.predOrder Set.ordConnected_Ici	—	Set.ordConnected_Ici coe_pred_of_mem Order.le_pred_of_lt lt_of_le_of_ne bot_le
pred_eq_of_not_isMin 📖	mathematical	IsMin Set.Elem Set.Ici PartialOrder.toPreorder Preorder.toLE Set Set.instMembership	Order.pred Subtype.preorder Set.OrdConnected.predOrder Set.ordConnected_Ici	—	Set.ordConnected_Ici coe_pred_of_not_isMin

Set.Iic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_succ_of_not_isMax 📖	mathematical	IsMax Set.Elem Set.Iic PartialOrder.toPreorder Preorder.toLE Set Set.instMembership	Order.succ Subtype.preorder Set.OrdConnected.succOrder Set.ordConnected_Iic	—	Set.ordConnected_Iic coe_succ_of_mem Order.succ_le_of_lt lt_of_le_of_ne le_top
succ_eq_of_not_isMax 📖	mathematical	IsMax Set.Elem Set.Iic PartialOrder.toPreorder Preorder.toLE Set Set.instMembership	Order.succ Subtype.preorder Set.OrdConnected.succOrder Set.ordConnected_Iic	—	Set.ordConnected_Iic coe_succ_of_not_isMax

(root)

Definitions

Name	Category	Theorems
SuccOrder 📖	CompData	2 math math: Order.instSubsingletonSuccOrder, WithBot.instIsEmptySuccOrderOfNonempty

---

← Back to Index