SuccPred

📁 Source: Mathlib/Order/Interval/Finset/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

Finset

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	—	coe_injective coe_Icc Order.Icc_pred_right coe_Ico
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	—	coe_injective coe_Icc coe_Ico Set.Icc_pred_right_eq_Ico_of_not_isMin
Icc_succ_left_eq_Ioc 📖	mathematical	—	Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Ioc	—	coe_injective coe_Icc Order.Icc_succ_left coe_Ioc
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	—	coe_injective coe_Icc coe_Ioc Set.Icc_succ_left_eq_Ioc_of_not_isMax
Icc_succ_pred_eq_Ioo 📖	mathematical	—	Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Order.pred Ioo	—	coe_injective coe_Icc coe_Ioo Set.Icc_succ_pred_eq_Ioo
Ici_succ_eq_Ioi 📖	mathematical	—	Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Ioi	—	coe_injective coe_Ici Order.Ici_succ coe_Ioi
Ici_succ_eq_Ioi_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ici Order.succ Ioi	—	coe_injective coe_Ici coe_Ioi Set.Ici_succ_eq_Ioi_of_not_isMax
Ico_succ_left_eq_Ioo 📖	mathematical	—	Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Ioo	—	coe_injective coe_Ico coe_Ioo Set.Ico_succ_left_eq_Ioo
Ico_succ_right_eq_Icc 📖	mathematical	—	Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Icc	—	coe_injective coe_Ico Order.Ico_succ_right coe_Icc
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	—	coe_injective coe_Ico coe_Icc Set.Ico_succ_right_eq_Icc_of_not_isMax
Ico_succ_succ_eq_Ioc 📖	mathematical	—	Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Ioc	—	coe_injective coe_Ico Order.Ico_succ_right Order.Icc_succ_left coe_Ioc
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	—	coe_injective coe_Ico coe_Ioc Set.Ico_succ_succ_eq_Ioc_of_not_isMax
Iic_pred_eq_Iio 📖	mathematical	—	Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Iio	—	coe_injective coe_Iic Order.Iic_pred coe_Iio
Iic_pred_eq_Iio_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Iic Order.pred Iio	—	coe_injective coe_Iic coe_Iio Set.Iic_pred_eq_Iio_of_not_isMin
Iio_succ_eq_Iic 📖	mathematical	—	Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Iic	—	coe_injective coe_Iio Order.Iio_succ coe_Iic
Iio_succ_eq_Iic_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Iio Order.succ Iic	—	coe_injective coe_Iio coe_Iic Set.Iio_succ_eq_Iic_of_not_isMax
Ioc_pred_left_eq_Icc 📖	mathematical	—	Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Icc	—	coe_injective coe_Ioc Order.Ioc_pred_left coe_Icc
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	—	coe_injective coe_Ioc coe_Icc Set.Ioc_pred_left_eq_Icc_of_not_isMin
Ioc_pred_pred_eq_Ico 📖	mathematical	—	Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Ico	—	coe_injective coe_Ioc Order.Ioc_pred_right Order.Ioo_pred_left coe_Ico
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	—	coe_injective coe_Ioc coe_Ico Set.Ioc_pred_pred_eq_Ico_of_not_isMin
Ioc_pred_right_eq_Ioo 📖	mathematical	—	Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Ioo	—	coe_injective coe_Ioc coe_Ioo Set.Ioc_pred_right_eq_Ioo
Ioi_pred_eq_Ici 📖	mathematical	—	Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Ici	—	coe_injective coe_Ioi Order.Ioi_pred coe_Ici
Ioi_pred_eq_Ici_of_not_isMin 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ioi Order.pred Ici	—	coe_injective coe_Ioi coe_Ici Set.Ioi_pred_eq_Ici_of_not_isMin
Ioo_pred_left_eq_Ioc 📖	mathematical	—	Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred Ico	—	coe_injective coe_Ioo Order.Ioo_pred_left coe_Ico
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	—	coe_injective coe_Ioo coe_Ico Set.Ioo_pred_left_eq_Ioc_of_not_isMin
Ioo_succ_right_eq_Ioc 📖	mathematical	—	Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ Ioc	—	coe_injective coe_Ioo Order.Ioo_succ_right coe_Ioc
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	—	coe_injective coe_Ioo coe_Ioc Set.Ioo_succ_right_eq_Ioc_of_not_isMax
insert_Icc_left_eq_Icc_pred 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.pred	Finset instInsert LinearOrder.toDecidableEq Icc	—	coe_injective coe_insert coe_Icc Set.insert_Icc_left_eq_Icc_pred
insert_Icc_pred_right_eq_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset instInsert LinearOrder.toDecidableEq Icc Order.pred	—	coe_injective coe_insert coe_Icc Set.insert_Icc_pred_right_eq_Icc
insert_Icc_right_eq_Icc_succ 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ	Finset instInsert LinearOrder.toDecidableEq Icc	—	coe_injective coe_insert coe_Icc Set.insert_Icc_right_eq_Icc_succ
insert_Icc_succ_left_eq_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset instInsert LinearOrder.toDecidableEq Icc Order.succ	—	coe_injective coe_insert coe_Icc Set.insert_Icc_succ_left_eq_Icc
insert_Ico_left_eq_Ico_pred 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset instInsert LinearOrder.toDecidableEq 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	Finset instInsert LinearOrder.toDecidableEq Order.pred Ico	—	coe_injective coe_insert coe_Ico Set.insert_Ico_left_eq_Ico_pred_of_not_isMin
insert_Ico_pred_right_eq_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset instInsert LinearOrder.toDecidableEq Order.pred Ico	—	coe_injective coe_insert coe_Ico Set.insert_Ico_pred_right_eq_Ico
insert_Ico_right_eq_Ico_succ 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset instInsert LinearOrder.toDecidableEq Ico Order.succ	—	coe_injective coe_insert coe_Ico Order.Ico_succ_right Set.insert_Ico_right_eq_Ico_succ
insert_Ico_right_eq_Ico_succ_of_not_isMax 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsMax	Finset instInsert LinearOrder.toDecidableEq Ico Order.succ	—	coe_injective coe_insert coe_Ico Set.insert_Ico_right_eq_Ico_succ_of_not_isMax
insert_Ico_succ_left_eq_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset instInsert LinearOrder.toDecidableEq Ico Order.succ	—	coe_injective coe_insert coe_Ico Set.insert_Ico_succ_left_eq_Ico
insert_Ioc_left_eq_Ioc_pred 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset instInsert LinearOrder.toDecidableEq Ioc Order.pred	—	coe_injective coe_insert coe_Ioc Order.Ioc_pred_left Set.insert_Ioc_left_eq_Ioc_pred
insert_Ioc_left_eq_Ioc_pred_of_not_isMin 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsMin	Finset instInsert LinearOrder.toDecidableEq Ioc Order.pred	—	coe_injective coe_insert coe_Ioc Set.insert_Ioc_left_eq_Ioc_pred_of_not_isMin
insert_Ioc_pred_right_eq_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset instInsert LinearOrder.toDecidableEq Ioc Order.pred	—	coe_injective coe_insert coe_Ioc Set.insert_Ioc_pred_right_eq_Ioc
insert_Ioc_right_eq_Ioc_succ 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset instInsert LinearOrder.toDecidableEq Order.succ Ioc	—	coe_injective coe_insert coe_Ioc Set.insert_Ioc_right_eq_Ioc_succ
insert_Ioc_right_eq_Ioc_succ_of_not_isMax 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsMax	Finset instInsert LinearOrder.toDecidableEq Order.succ Ioc	—	coe_injective coe_insert coe_Ioc Set.insert_Ioc_right_eq_Ioc_succ_of_not_isMax
insert_Ioc_succ_left_eq_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset instInsert LinearOrder.toDecidableEq Order.succ Ioc	—	coe_injective coe_insert coe_Ioc Set.insert_Ioc_succ_left_eq_Ioc

---

← Back to Index