DenselyOrdered

📁 Source: Mathlib/Order/Interval/Finset/DenselyOrdered.lean

Statistics

Metric	Count
Definitions	0
Theorems denselyOrdered_iff_subsingleton, denselyOrdered_set_iff_subsingleton, denselyOrdered_set_iff_subsingleton, denselyOrdered_set_iff_subsingleton	4
Total	4

LocallyFiniteOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denselyOrdered_iff_subsingleton 📖	mathematical	—	DenselyOrdered Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	not_nontrivial_iff_subsingleton nontrivial_iff_lt not_lt_of_denselyOrdered_of_locallyFinite Subsingleton.instDenselyOrdered

WithBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denselyOrdered_set_iff_subsingleton 📖	mathematical	—	DenselyOrdered Set.Elem WithBot Preorder.toLT instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Subsingleton	—	Set.subsingleton_coe not_nontrivial_iff_subsingleton nontrivial_iff_lt exists_between LT.lt.ne' LT.lt.trans_le' coe_unbot coe_lt_coe LT.lt.trans_le Subtype.coe_lt_coe LT.lt.trans denselyOrdered_set_iff_subsingleton LT.lt.ne Set.Subsingleton.denselyOrdered

WithTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denselyOrdered_set_iff_subsingleton 📖	mathematical	—	DenselyOrdered Set.Elem WithTop Preorder.toLT instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Subsingleton	—	Equiv.image_strictAnti denselyOrdered_iff_of_strictAnti WithBot.denselyOrdered_set_iff_subsingleton Function.Injective.subsingleton_image_iff Equiv.injective

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denselyOrdered_set_iff_subsingleton 📖	mathematical	—	DenselyOrdered Set.Elem Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Subsingleton	—	—

---

← Back to Index