Relation

📁 Source: Mathlib/Order/SuccPred/Relation.lean

Statistics

Metric	Count
Definitions Relation, Relation, Relation, Relation, Relation	5
Theorems reflTransGen_of_pred, reflTransGen_of_pred_of_ge, reflTransGen_of_pred_of_le, reflTransGen_of_succ, reflTransGen_of_succ_of_ge, reflTransGen_of_succ_of_le, transGen_of_pred_of_gt, transGen_of_pred_of_lt, transGen_of_pred_of_ne, transGen_of_pred_of_reflexive, transGen_of_succ_of_gt, transGen_of_succ_of_lt, transGen_of_succ_of_ne, transGen_of_succ_of_reflexive	14
Total	19

CategoryTheory.GrothendieckTopology.Cover

Definitions

Name	Category	Theorems
Relation 📖	CompData	1 math math: shape_R

CategoryTheory.GrothendieckTopology.Cover.Arrow

Definitions

Name	Category	Theorems
Relation 📖	CompData	2 math math: CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₁, CategoryTheory.GrothendieckTopology.Cover.Relation.ext_iff

CommRingCat.Colimits

Definitions

Name	Category	Theorems
Relation 📖	CompData	—

MonCat.Colimits

Definitions

Name	Category	Theorems
Relation 📖	CompData	—

RingCat.Colimits

Definitions

Name	Category	Theorems
Relation 📖	CompData	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflTransGen_of_pred 📖	mathematical	Order.pred PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Relation.ReflTransGen	—	reflTransGen_of_succ instIsSuccArchimedeanOrderDual
reflTransGen_of_pred_of_ge 📖	mathematical	Order.pred PartialOrder.toPreorder Preorder.toLE	Relation.ReflTransGen	—	reflTransGen_of_succ_of_le instIsSuccArchimedeanOrderDual
reflTransGen_of_pred_of_le 📖	mathematical	Order.pred PartialOrder.toPreorder Preorder.toLE	Relation.ReflTransGen	—	reflTransGen_of_succ_of_ge instIsSuccArchimedeanOrderDual
reflTransGen_of_succ 📖	mathematical	Order.succ PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Relation.ReflTransGen	—	le_total reflTransGen_of_succ_of_le reflTransGen_of_succ_of_ge
reflTransGen_of_succ_of_ge 📖	mathematical	Order.succ PartialOrder.toPreorder Preorder.toLE	Relation.ReflTransGen	—	Relation.reflTransGen_swap reflTransGen_of_succ_of_le
reflTransGen_of_succ_of_le 📖	mathematical	Order.succ PartialOrder.toPreorder Preorder.toLE	Relation.ReflTransGen	—	LT.lt.trans_le Order.le_succ LE.le.eq_or_lt
transGen_of_pred_of_gt 📖	—	Order.pred PartialOrder.toPreorder Preorder.toLT	—	—	transGen_of_succ_of_lt instIsSuccArchimedeanOrderDual
transGen_of_pred_of_lt 📖	—	Order.pred PartialOrder.toPreorder Preorder.toLT	—	—	transGen_of_succ_of_gt instIsSuccArchimedeanOrderDual
transGen_of_pred_of_ne 📖	—	Order.pred PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	transGen_of_succ_of_ne instIsSuccArchimedeanOrderDual
transGen_of_pred_of_reflexive 📖	—	Reflexive Order.pred PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	transGen_of_succ_of_reflexive instIsSuccArchimedeanOrderDual
transGen_of_succ_of_gt 📖	—	Order.succ PartialOrder.toPreorder Preorder.toLT	—	—	Relation.reflTransGen_iff_eq_or_transGen reflTransGen_of_succ_of_ge LT.lt.le LT.lt.ne
transGen_of_succ_of_lt 📖	—	Order.succ PartialOrder.toPreorder Preorder.toLT	—	—	Relation.reflTransGen_iff_eq_or_transGen reflTransGen_of_succ_of_le LT.lt.le LT.lt.ne'
transGen_of_succ_of_ne 📖	—	Order.succ PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	Relation.reflTransGen_iff_eq_or_transGen reflTransGen_of_succ
transGen_of_succ_of_reflexive 📖	—	Reflexive Order.succ PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	eq_or_ne transGen_of_succ_of_ne

---

← Back to Index