SuccPred

📁 Source: Mathlib/Algebra/Order/Interval/Set/SuccPred.lean

Statistics

Metric	Count
Definitions	0
Theorems Icc_add_one_left_eq_Ioc, Icc_add_one_left_eq_Ioc_of_not_isMax, Icc_add_one_sub_one_eq_Ioo, Icc_sub_one_right_eq_Ico, Icc_sub_one_right_eq_Ico_of_not_isMin, Ici_add_one_eq_Ioi, Ici_add_one_eq_Ioi_of_not_isMax, Ico_add_one_add_one_eq_Ioc, Ico_add_one_add_one_eq_Ioc_of_not_isMax, Ico_add_one_left_eq_Ioo, Ico_add_one_right_eq_Icc, Ico_add_one_right_eq_Icc_of_not_isMax, Iic_sub_one_eq_Iio, Iic_sub_one_eq_Iio_of_not_isMin, Iio_add_one_eq_Iic, Iio_add_one_eq_Iic_of_not_isMax, Ioc_sub_one_left_eq_Icc, Ioc_sub_one_left_eq_Icc_of_not_isMin, Ioc_sub_one_right_eq_Ioo, Ioc_sub_one_sub_one_eq_Ico, Ioc_sub_one_sub_one_eq_Ico_of_not_isMin, Ioi_sub_one_eq_Ici, Ioi_sub_one_eq_Ici_of_not_isMin, Ioo_add_one_right_eq_Ioc, Ioo_add_one_right_eq_Ioc_of_not_isMax, Ioo_sub_one_left_eq_Ioc, Ioo_sub_one_left_eq_Ioc_of_not_isMin, insert_Icc_add_one_left_eq_Icc, insert_Icc_left_eq_Icc_sub_one, insert_Icc_right_eq_Icc_add_one, insert_Icc_sub_one_right_eq_Icc, insert_Ico_add_one_left_eq_Ico, insert_Ico_left_eq_Ico_sub_one, insert_Ico_left_eq_Ico_sub_one_of_not_isMin, insert_Ico_right_eq_Ico_add_one, insert_Ico_right_eq_Ico_add_one_of_not_isMax, insert_Ico_sub_one_right_eq_Ico, insert_Ioc_add_one_left_eq_Ioc, insert_Ioc_left_eq_Ioc_sub_one, insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin, insert_Ioc_right_eq_Ioc_add_one, insert_Ioc_right_eq_Ioc_add_one_of_not_isMax, insert_Ioc_sub_one_right_eq_Ioc	43
Total	43

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_add_one_left_eq_Ioc 📖	mathematical	—	Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc	—	Order.succ_eq_add_one Icc_succ_left_eq_Ioc
Icc_add_one_left_eq_Ioc_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Icc Ioc	—	Order.succ_eq_add_one Icc_succ_left_eq_Ioc_of_not_isMax
Icc_add_one_sub_one_eq_Ioo 📖	mathematical	—	Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo	—	Order.succ_eq_add_one Order.pred_eq_sub_one Icc_succ_pred_eq_Ioo
Icc_sub_one_right_eq_Ico 📖	mathematical	—	Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico	—	Order.pred_eq_sub_one Icc_pred_right_eq_Ico
Icc_sub_one_right_eq_Ico_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Icc Ico	—	Order.pred_eq_sub_one Icc_pred_right_eq_Ico_of_not_isMin
Ici_add_one_eq_Ioi 📖	mathematical	—	Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi	—	Order.succ_eq_add_one Ici_succ_eq_Ioi
Ici_add_one_eq_Ioi_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ici Ioi	—	Order.succ_eq_add_one Ici_succ_eq_Ioi_of_not_isMax
Ico_add_one_add_one_eq_Ioc 📖	mathematical	—	Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc	—	Order.succ_eq_add_one Ico_succ_succ_eq_Ioc
Ico_add_one_add_one_eq_Ioc_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ico Ioc	—	Order.succ_eq_add_one Ico_succ_succ_eq_Ioc_of_not_isMax
Ico_add_one_left_eq_Ioo 📖	mathematical	—	Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo	—	Order.succ_eq_add_one Ico_succ_left_eq_Ioo
Ico_add_one_right_eq_Icc 📖	mathematical	—	Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Icc	—	Order.succ_eq_add_one Ico_succ_right_eq_Icc
Ico_add_one_right_eq_Icc_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ico Icc	—	Order.succ_eq_add_one Ico_succ_right_eq_Icc_of_not_isMax
Iic_sub_one_eq_Iio 📖	mathematical	—	Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Iio	—	Order.pred_eq_sub_one Iic_pred_eq_Iio
Iic_sub_one_eq_Iio_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Iic Iio	—	Order.pred_eq_sub_one Iic_pred_eq_Iio_of_not_isMin
Iio_add_one_eq_Iic 📖	mathematical	—	Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Iic	—	Order.succ_eq_add_one Iio_succ_eq_Iic
Iio_add_one_eq_Iic_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Iio Iic	—	Order.succ_eq_add_one Iio_succ_eq_Iic_of_not_isMax
Ioc_sub_one_left_eq_Icc 📖	mathematical	—	Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Icc	—	Order.pred_eq_sub_one Ioc_pred_left_eq_Icc
Ioc_sub_one_left_eq_Icc_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ioc Icc	—	Order.pred_eq_sub_one Ioc_pred_left_eq_Icc_of_not_isMin
Ioc_sub_one_right_eq_Ioo 📖	mathematical	—	Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo	—	Order.pred_eq_sub_one Ioc_pred_right_eq_Ioo
Ioc_sub_one_sub_one_eq_Ico 📖	mathematical	—	Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico	—	Order.pred_eq_sub_one Ioc_pred_pred_eq_Ico
Ioc_sub_one_sub_one_eq_Ico_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ioc Ico	—	Order.pred_eq_sub_one Ioc_pred_pred_eq_Ico_of_not_isMin
Ioi_sub_one_eq_Ici 📖	mathematical	—	Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici	—	Order.pred_eq_sub_one Ioi_pred_eq_Ici
Ioi_sub_one_eq_Ici_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ioi Ici	—	Order.pred_eq_sub_one Ioi_pred_eq_Ici_of_not_isMin
Ioo_add_one_right_eq_Ioc 📖	mathematical	—	Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc	—	Order.succ_eq_add_one Ioo_succ_right_eq_Ioc
Ioo_add_one_right_eq_Ioc_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ioo Ioc	—	Order.succ_eq_add_one Ioo_succ_right_eq_Ioc_of_not_isMax
Ioo_sub_one_left_eq_Ioc 📖	mathematical	—	Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico	—	Order.pred_eq_sub_one Ioo_pred_left_eq_Ioc
Ioo_sub_one_left_eq_Ioc_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ioo Ico	—	Order.pred_eq_sub_one Ioo_pred_left_eq_Ioc_of_not_isMin
insert_Icc_add_one_left_eq_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Icc	—	Order.succ_eq_add_one insert_Icc_succ_left_eq_Icc
insert_Icc_left_eq_Icc_sub_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Icc	—	insert_Icc_left_eq_Icc_pred Order.pred_eq_sub_one
insert_Icc_right_eq_Icc_add_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Icc	—	insert_Icc_right_eq_Icc_succ Order.succ_eq_add_one
insert_Icc_sub_one_right_eq_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Icc	—	Order.pred_eq_sub_one insert_Icc_pred_right_eq_Icc
insert_Ico_add_one_left_eq_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Ico	—	Order.succ_eq_add_one insert_Ico_succ_left_eq_Ico
insert_Ico_left_eq_Ico_sub_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Ico	—	insert_Ico_left_eq_Ico_sub_one_of_not_isMin not_isMin
insert_Ico_left_eq_Ico_sub_one_of_not_isMin 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsMin	Set instInsert Ico	—	Order.pred_eq_sub_one insert_Ico_left_eq_Ico_pred_of_not_isMin
insert_Ico_right_eq_Ico_add_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Ico	—	Order.succ_eq_add_one insert_Ico_right_eq_Ico_succ
insert_Ico_right_eq_Ico_add_one_of_not_isMax 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsMax	Set instInsert Ico	—	Order.succ_eq_add_one insert_Ico_right_eq_Ico_succ_of_not_isMax
insert_Ico_sub_one_right_eq_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Ico	—	Order.pred_eq_sub_one insert_Ico_pred_right_eq_Ico
insert_Ioc_add_one_left_eq_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Ioc	—	Order.succ_eq_add_one insert_Ioc_succ_left_eq_Ioc
insert_Ioc_left_eq_Ioc_sub_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Ioc	—	Order.pred_eq_sub_one insert_Ioc_left_eq_Ioc_pred
insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsMin	Set instInsert Ioc	—	Order.pred_eq_sub_one insert_Ioc_left_eq_Ioc_pred_of_not_isMin
insert_Ioc_right_eq_Ioc_add_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Ioc	—	insert_Ioc_right_eq_Ioc_add_one_of_not_isMax not_isMax
insert_Ioc_right_eq_Ioc_add_one_of_not_isMax 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsMax	Set instInsert Ioc	—	Order.succ_eq_add_one insert_Ioc_right_eq_Ioc_succ_of_not_isMax
insert_Ioc_sub_one_right_eq_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Ioc	—	Order.pred_eq_sub_one insert_Ioc_pred_right_eq_Ioc

---

← Back to Index