SuccPred

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

Statistics

Metric	Count
Definitions	0
Theorems Icc_pred_right_eq_Ico, Icc_pred_right_eq_Ico_of_not_isMin, Icc_succ_left_eq_Ioc, Icc_succ_left_eq_Ioc_of_not_isMax, Icc_succ_pred_eq_Ioo, Ici_succ_eq_Ioi, Ici_succ_eq_Ioi_of_not_isMax, Ico_succ_left_eq_Ioo, Ico_succ_right_eq_Icc, Ico_succ_right_eq_Icc_of_not_isMax, Ico_succ_succ_eq_Ioc, Ico_succ_succ_eq_Ioc_of_not_isMax, Iic_pred_eq_Iio, Iic_pred_eq_Iio_of_not_isMin, Iio_succ_eq_Iic, Iio_succ_eq_Iic_of_not_isMax, Ioc_pred_left_eq_Icc, Ioc_pred_left_eq_Icc_of_not_isMin, Ioc_pred_pred_eq_Ico, Ioc_pred_pred_eq_Ico_of_not_isMin, Ioc_pred_right_eq_Ioo, Ioi_pred_eq_Ici, Ioi_pred_eq_Ici_of_not_isMin, Ioo_pred_left_eq_Ioc, Ioo_pred_left_eq_Ioc_of_not_isMin, Ioo_succ_right_eq_Ioc, Ioo_succ_right_eq_Ioc_of_not_isMax, insert_Icc_left_eq_Icc_pred, insert_Icc_pred_right_eq_Icc, insert_Icc_right_eq_Icc_succ, insert_Icc_succ_left_eq_Icc, insert_Ico_left_eq_Ico_pred, insert_Ico_left_eq_Ico_pred_of_not_isMin, insert_Ico_pred_right_eq_Ico, insert_Ico_right_eq_Ico_succ, insert_Ico_right_eq_Ico_succ_of_not_isMax, insert_Ico_succ_left_eq_Ico, insert_Ioc_left_eq_Ioc_pred, insert_Ioc_left_eq_Ioc_pred_of_not_isMin, insert_Ioc_pred_right_eq_Ioc, insert_Ioc_right_eq_Ioc_succ, insert_Ioc_right_eq_Ioc_succ_of_not_isMax, insert_Ioc_succ_left_eq_Ioc	43
Total	43

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_pred_right_eq_Ico 📖	mathematical	—	Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Ico	—	Icc_pred_right_eq_Ico_of_not_isMin not_isMin
Icc_pred_right_eq_Ico_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Icc Order.pred Ico	—	ext mem_Icc mem_Ico Order.le_pred_iff_of_not_isMin
Icc_succ_left_eq_Ioc 📖	mathematical	—	Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Ioc	—	Icc_succ_left_eq_Ioc_of_not_isMax not_isMax
Icc_succ_left_eq_Ioc_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Icc Order.succ Ioc	—	ext mem_Icc mem_Ioc Order.succ_le_iff_of_not_isMax
Icc_succ_pred_eq_Ioo 📖	mathematical	—	Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Order.pred Ioo	—	Icc_eq_empty Order.not_isMin_succ IsMin.mono LE.le.trans Order.pred_le Ioo_eq_empty IsMin.not_lt Icc_pred_right_eq_Ico_of_not_isMin Ico_succ_left_eq_Ioo
Ici_succ_eq_Ioi 📖	mathematical	—	Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Ioi	—	Ici_succ_eq_Ioi_of_not_isMax not_isMax
Ici_succ_eq_Ioi_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ici Order.succ Ioi	—	ext mem_Ici mem_Ioi Order.succ_le_iff_of_not_isMax
Ico_succ_left_eq_Ioo 📖	mathematical	—	Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Ioo	—	Ico_eq_empty IsMax.not_lt IsMax.mono Order.le_succ Ioo_eq_empty ext mem_Ico mem_Ioo Order.succ_le_iff_of_not_isMax
Ico_succ_right_eq_Icc 📖	mathematical	—	Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Icc	—	Ico_succ_right_eq_Icc_of_not_isMax not_isMax
Ico_succ_right_eq_Icc_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ico Order.succ Icc	—	ext mem_Ico mem_Icc Order.lt_succ_iff_of_not_isMax
Ico_succ_succ_eq_Ioc 📖	mathematical	—	Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Ioc	—	Ico_succ_succ_eq_Ioc_of_not_isMax not_isMax
Ico_succ_succ_eq_Ioc_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ico Order.succ Ioc	—	Ico_succ_left_eq_Ioo Ioo_succ_right_eq_Ioc_of_not_isMax
Iic_pred_eq_Iio 📖	mathematical	—	Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Iio	—	Iic_pred_eq_Iio_of_not_isMin not_isMin
Iic_pred_eq_Iio_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Iic Order.pred Iio	—	ext mem_Iic mem_Iio Order.le_pred_iff_of_not_isMin
Iio_succ_eq_Iic 📖	mathematical	—	Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Iic	—	Iio_succ_eq_Iic_of_not_isMax not_isMax
Iio_succ_eq_Iic_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Iio Order.succ Iic	—	ext mem_Iio mem_Iic Order.lt_succ_iff_of_not_isMax
Ioc_pred_left_eq_Icc 📖	mathematical	—	Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Icc	—	Ioc_pred_left_eq_Icc_of_not_isMin not_isMin
Ioc_pred_left_eq_Icc_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ioc Order.pred Icc	—	ext mem_Ioc mem_Icc Order.pred_lt_iff_of_not_isMin
Ioc_pred_pred_eq_Ico 📖	mathematical	—	Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Ico	—	Ioc_pred_pred_eq_Ico_of_not_isMin not_isMin
Ioc_pred_pred_eq_Ico_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ioc Order.pred Ico	—	Ioc_pred_right_eq_Ioo Ioo_pred_left_eq_Ioc_of_not_isMin
Ioc_pred_right_eq_Ioo 📖	mathematical	—	Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Ioo	—	Ioc_eq_empty IsMin.not_lt IsMin.mono Order.pred_le Ioo_eq_empty ext mem_Ioc mem_Ioo Order.le_pred_iff_of_not_isMin
Ioi_pred_eq_Ici 📖	mathematical	—	Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Ici	—	Ioi_pred_eq_Ici_of_not_isMin not_isMin
Ioi_pred_eq_Ici_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ioi Order.pred Ici	—	ext mem_Ioi mem_Ici Order.pred_lt_iff_of_not_isMin
Ioo_pred_left_eq_Ioc 📖	mathematical	—	Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Ico	—	Ioo_pred_left_eq_Ioc_of_not_isMin not_isMin
Ioo_pred_left_eq_Ioc_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ioo Order.pred Ico	—	ext mem_Ioo mem_Ico Order.pred_lt_iff_of_not_isMin
Ioo_succ_right_eq_Ioc 📖	mathematical	—	Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Ioc	—	Ioo_succ_right_eq_Ioc_of_not_isMax not_isMax
Ioo_succ_right_eq_Ioc_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ioo Order.succ Ioc	—	ext mem_Ioo mem_Ioc Order.lt_succ_iff_of_not_isMax
insert_Icc_left_eq_Icc_pred 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred	Set instInsert Icc	—	ext
insert_Icc_pred_right_eq_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Icc Order.pred	—	ext
insert_Icc_right_eq_Icc_succ 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ	Set instInsert Icc	—	ext
insert_Icc_succ_left_eq_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Icc Order.succ	—	ext
insert_Ico_left_eq_Ico_pred 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Order.pred Ico	—	insert_Ico_left_eq_Ico_pred_of_not_isMin not_isMin
insert_Ico_left_eq_Ico_pred_of_not_isMin 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsMin	Set instInsert Order.pred Ico	—	ext Order.pred_lt_of_le_of_not_isMin
insert_Ico_pred_right_eq_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Order.pred Ico	—	Ico_insert_right Order.le_pred_of_lt Order.Icc_pred_right_of_not_isMin LT.lt.not_isMin
insert_Ico_right_eq_Ico_succ 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Ico Order.succ	—	insert_Ico_right_eq_Ico_succ_of_not_isMax not_isMax
insert_Ico_right_eq_Ico_succ_of_not_isMax 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsMax	Set instInsert Ico Order.succ	—	Order.Ico_succ_right_of_not_isMax Ico_insert_right
insert_Ico_succ_left_eq_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Ico Order.succ	—	Order.Ico_succ_left_of_not_isMax LT.lt.not_isMax Ioo_insert_left
insert_Ioc_left_eq_Ioc_pred 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Ioc Order.pred	—	insert_Ioc_left_eq_Ioc_pred_of_not_isMin not_isMin
insert_Ioc_left_eq_Ioc_pred_of_not_isMin 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsMin	Set instInsert Ioc Order.pred	—	Order.Ioc_pred_left_of_not_isMin Ioc_insert_left
insert_Ioc_pred_right_eq_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Ioc Order.pred	—	Order.Ioc_pred_right_of_not_isMin LT.lt.not_isMin Ioo_insert_right
insert_Ioc_right_eq_Ioc_succ 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Order.succ Ioc	—	insert_Ioc_right_eq_Ioc_succ_of_not_isMax not_isMax
insert_Ioc_right_eq_Ioc_succ_of_not_isMax 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsMax	Set instInsert Order.succ Ioc	—	ext Order.lt_succ_of_le_of_not_isMax
insert_Ioc_succ_left_eq_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInsert Order.succ Ioc	—	Ioc_insert_left Order.succ_le_of_lt Order.Icc_succ_left_of_not_isMax LT.lt.not_isMax

---

← Back to Index