Documentation Verification Report

CountableDenseLinearOrder

📁 Source: Mathlib/Order/CountableDenseLinearOrder.lean

Statistics

Metric	Count
Definitions `PartialIso`, `comm`, `definedAtLeft`, `definedAtRight`, `funOfIdeal`, `instInhabited`, `instPreorder`, `invOfIdeal`	8
Theorems `exists_across`, `embedding_from_countable_to_dense`, `exists_between_finsets`, `exists_orderEmbedding_insert`, `iso_of_countable_dense`	5
Total	13

Order

Definitions

Name	Category	Theorems
`PartialIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`embedding_from_countable_to_dense` 📖	mathematical	—	`OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`nonempty_encodable` `exists_pair_lt` `exists_between` `Set.instDenselyOrdered` `Set.ordConnected_Ioo` `instNoMinOrderElemIoo` `instNoMaxOrderElemIoo` `cofinal_meets_idealOfCofinals` `Subtype.prop` `Ideal.directed` `lt_iff_lt_of_cmp_eq_cmp`
`exists_between_finsets` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`exists_between` `Finset.max'_mem` `Finset.min'_mem` `lt_of_le_of_lt` `Finset.le_max'` `lt_of_lt_of_le` `Finset.min'_le` `NoMaxOrder.exists_gt` `NoMinOrder.exists_lt`
`exists_orderEmbedding_insert` 📖	mathematical	—	`Set.Elem` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership` `Finset.instInsert` `LinearOrder.toDecidableEq` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding` `Set.inclusion` `Finset.subset_insert`	—	`Finset.subset_insert` `exists_between_finsets` `OrderEmbedding.strictMono` `LT.lt.trans` `Finset.mem_image_of_mem` `Finset.mem_filter` `Finset.mem_attach` `Finset.eq_of_mem_insert_of_notMem` `Subtype.coe_eta`
`iso_of_countable_dense` 📖	mathematical	—	`OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`nonempty_encodable` `cofinal_meets_idealOfCofinals` `Subtype.prop` `Ideal.directed`

Order.PartialIso

Definitions

Name	Category	Theorems
`comm` 📖	CompOp	—
`definedAtLeft` 📖	CompOp	—
`definedAtRight` 📖	CompOp	—
`funOfIdeal` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instPreorder` 📖	CompOp	—
`invOfIdeal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_across` 📖	mathematical	—	`cmp` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLT`	—	`Subtype.prop` `Finset.mem_image` `lt_iff_lt_of_cmp_eq_cmp` `Finset.mem_filter` `lt_trans` `Order.exists_between_finsets` `lt_or_gt_of_ne` `cmp_eq_lt_iff` `cmp_eq_gt_iff`

---

← Back to Index