DenselyOrdered

📁 Source: Mathlib/Data/Finset/DenselyOrdered.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_between, exists_between', exists_between, exists_between'	4
Total	4

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_between 📖	—	Nonempty Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	exists_between
exists_between' 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	exists_between NoMaxOrder.exists_gt instIsEmptyFalse NoMinOrder.exists_lt

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_between 📖	—	Set.Nonempty Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	Finset.exists_between
exists_between' 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	Finset.exists_between'

---

← Back to Index