Documentation Verification Report

LinearLocallyFinite

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

Statistics

Metric	Count
Definitions `predOrder`, `succFn`, `succOrder`, `orderIsoIntOfLinearSuccPredArch`, `orderIsoNatOfLinearSuccPredArch`, `orderIsoRangeOfLinearSuccPredArch`, `orderIsoRangeToZOfLinearSuccPredArch`, `toZ`	8
Theorems `of_linearOrder_locallyFiniteOrder`, `instIsPredArchimedeanOfLocallyFiniteOrder`, `instIsSuccArchimedeanOfLocallyFiniteOrder`, `isGLB_Ioc_of_isGLB_Ioi`, `isMax_of_succFn_le`, `le_of_lt_succFn`, `le_succFn`, `succFn_le_of_lt`, `succFn_spec`, `isPredArchimedean_of_isSuccArchimedean`, `isSuccArchimedean_iff_isPredArchimedean`, `isSuccArchimedean_of_isPredArchimedean`, `countable_of_linear_succ_pred_arch`, `injective_toZ`, `iterate_pred_toZ`, `iterate_succ_toZ`, `le_of_toZ_le`, `toZ_iterate_pred`, `toZ_iterate_pred_ge`, `toZ_iterate_pred_of_not_isMin`, `toZ_iterate_succ`, `toZ_iterate_succ_le`, `toZ_iterate_succ_of_not_isMax`, `toZ_le_iff`, `toZ_mono`, `toZ_neg`, `toZ_nonneg`, `toZ_of_eq`, `toZ_of_ge`, `toZ_of_lt`	30
Total	38

Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_linearOrder_locallyFiniteOrder` 📖	mathematical	—	`Countable`	—	`countable_of_linear_succ_pred_arch` `LinearOrder.isSuccArchimedean_of_isPredArchimedean` `LinearLocallyFiniteOrder.instIsPredArchimedeanOfLocallyFiniteOrder`

LinearLocallyFiniteOrder

Definitions

Name	Category	Theorems
`predOrder` 📖	CompOp	—
`succFn` 📖	CompOp	3 math math: `succFn_le_of_lt`, `succFn_spec`, `le_succFn`
`succOrder` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsPredArchimedeanOfLocallyFiniteOrder` 📖	mathematical	—	`IsPredArchimedean` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`instIsPredArchimedeanOrderDual` `instIsSuccArchimedeanOfLocallyFiniteOrder`
`instIsSuccArchimedeanOfLocallyFiniteOrder` 📖	mathematical	—	`IsSuccArchimedean` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_iff_lt_or_eq` `lt_of_le_of_ne` `Function.iterate_succ'` `Order.succ_le_of_lt` `Finset.mem_Icc` `Order.le_succ_iterate` `LT.lt.le` `Finite.exists_ne_map_eq_of_infinite` `instInfiniteNat` `Finite.of_fintype` `le_total` `Order.isMax_iterate_succ_of_eq_of_ne` `LT.lt.ne` `not_le`
`isGLB_Ioc_of_isGLB_Ioi` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsGLB` `Preorder.toLE` `Set.Ioi`	`Set.Ioc`	—	`le_or_gt` `le_trans` `le_rfl` `LT.lt.le`
`isMax_of_succFn_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `succFn`	`IsMax`	—	`not_lt` `le_antisymm` `le_succFn` `Finset.coe_Ioc` `succFn_spec` `isGLB_Ioc_of_isGLB_Ioi` `Finset.isGLB_mem` `Finset.mem_Ioc` `le_rfl` `lt_irrefl`
`le_of_lt_succFn` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `succFn`	`Preorder.toLE`	—	`lt_isGLB_iff` `succFn_spec` `not_lt` `not_le` `mem_lowerBounds`
`le_succFn` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `succFn`	—	`le_isGLB_iff` `succFn_spec` `mem_lowerBounds` `le_of_lt`
`succFn_le_of_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `succFn`	—	`succFn_spec` `mem_lowerBounds` `IsGreatest.eq_1` `IsGLB.eq_1`
`succFn_spec` 📖	mathematical	—	`IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi` `succFn`	—	`exists_glb_Ioi`

LinearOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPredArchimedean_of_isSuccArchimedean` 📖	mathematical	—	`IsPredArchimedean` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsSuccArchimedean.exists_succ_iterate_of_le` `Nat.find_spec` `Nat.find_min` `Order.pred_succ_iterate_of_not_isMax` `tsub_zero` `Nat.instOrderedSub` `lt_of_le_of_ne` `Function.iterate_succ_apply'` `Order.le_succ` `not_isMax_of_lt`
`isSuccArchimedean_iff_isPredArchimedean` 📖	mathematical	—	`IsSuccArchimedean` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsPredArchimedean`	—	`isPredArchimedean_of_isSuccArchimedean` `isSuccArchimedean_of_isPredArchimedean`
`isSuccArchimedean_of_isPredArchimedean` 📖	mathematical	—	`IsSuccArchimedean` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`instIsSuccArchimedeanOrderDual` `isPredArchimedean_of_isSuccArchimedean`

(root)

Definitions

Name	Category	Theorems
`orderIsoIntOfLinearSuccPredArch` 📖	CompOp	—
`orderIsoNatOfLinearSuccPredArch` 📖	CompOp	—
`orderIsoRangeOfLinearSuccPredArch` 📖	CompOp	—
`orderIsoRangeToZOfLinearSuccPredArch` 📖	CompOp	—
`toZ` 📖	CompOp	16 math math: `toZ_of_eq`, `toZ_iterate_succ_of_not_isMax`, `toZ_iterate_pred_of_not_isMin`, `toZ_of_ge`, `injective_toZ`, `iterate_pred_toZ`, `toZ_iterate_pred_ge`, `toZ_nonneg`, `toZ_iterate_succ`, `toZ_iterate_pred`, `toZ_neg`, `toZ_iterate_succ_le`, `iterate_succ_toZ`, `toZ_of_lt`, `toZ_mono`, `toZ_le_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countable_of_linear_succ_pred_arch` 📖	mathematical	—	`Countable`	—	`isEmpty_or_nonempty` `Encodable.countable` `Countable.of_equiv` `SetCoe.countable` `instCountableInt`
`injective_toZ` 📖	mathematical	—	`toZ`	—	`le_antisymm` `le_of_toZ_le` `Eq.le`
`iterate_pred_toZ` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Nat.iterate` `Order.pred` `toZ`	—	`IsPredArchimedean.exists_pred_iterate_of_le` `LinearOrder.isPredArchimedean_of_isSuccArchimedean` `LT.lt.le` `toZ_of_lt` `neg_neg` `Nat.find_spec`
`iterate_succ_toZ` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Nat.iterate` `Order.succ` `toZ`	—	`IsSuccArchimedean.exists_succ_iterate_of_le` `toZ_of_ge` `Nat.find_spec`
`le_of_toZ_le` 📖	mathematical	`toZ`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_or_gt` `iterate_succ_toZ` `Monotone.monotone_iterate_of_le_map` `Order.succ_mono` `Order.le_succ` `LT.lt.trans_le` `toZ_neg` `toZ_nonneg` `not_lt` `LE.le.trans` `LT.lt.le` `iterate_pred_toZ` `Monotone.antitone_iterate_of_map_le` `Order.pred_mono` `Order.pred_le`
`toZ_iterate_pred` 📖	mathematical	—	`toZ` `Nat.iterate` `Order.pred` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`toZ_iterate_pred_of_not_isMin` `not_isMin`
`toZ_iterate_pred_ge` 📖	mathematical	—	`toZ` `Nat.iterate` `Order.pred` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_or_gt` `le_antisymm` `Order.pred_iterate_le` `toZ_of_eq` `IsPredArchimedean.exists_pred_iterate_of_le` `LinearOrder.isPredArchimedean_of_isSuccArchimedean` `LT.lt.le` `toZ_of_lt` `Nat.find_min'`
`toZ_iterate_pred_of_not_isMin` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nat.iterate` `Order.pred`	`toZ`	—	`toZ_of_eq` `neg_zero` `lt_of_le_of_ne` `Order.pred_iterate_le` `Function.iterate_zero` `Order.isMin_iterate_pred_of_eq_of_ne` `iterate_pred_toZ` `IsPredArchimedean.exists_pred_iterate_of_le` `LinearOrder.isPredArchimedean_of_isSuccArchimedean` `LT.lt.le` `toZ_of_lt` `max_eq_left` `neg_neg`
`toZ_iterate_succ` 📖	mathematical	—	`toZ` `Nat.iterate` `Order.succ` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`toZ_iterate_succ_of_not_isMax` `not_isMax`
`toZ_iterate_succ_le` 📖	mathematical	—	`toZ` `Nat.iterate` `Order.succ` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsSuccArchimedean.exists_succ_iterate_of_le` `Order.le_succ_iterate` `toZ_of_ge` `Nat.find_min'`
`toZ_iterate_succ_of_not_isMax` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nat.iterate` `Order.succ`	`toZ`	—	`iterate_succ_toZ` `Order.le_succ_iterate` `IsSuccArchimedean.exists_succ_iterate_of_le` `toZ_of_ge` `max_eq_left` `Order.isMax_iterate_succ_of_eq_of_ne`
`toZ_le_iff` 📖	mathematical	—	`toZ` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_of_toZ_le` `toZ_mono`
`toZ_mono` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`toZ`	—	`le_antisymm` `le_refl` `le_or_gt` `IsSuccArchimedean.exists_succ_iterate_of_le` `Nat.find_spec` `add_comm` `iterate_succ_toZ` `Function.iterate_add` `Function.iterate_zero` `le_of_eq` `Order.max_of_succ_le` `le_trans` `Monotone.monotone_iterate_of_le_map` `Order.succ_mono` `Order.le_succ` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Function.iterate_succ'` `le_of_toZ_le` `le_of_not_ge` `not_le` `LT.lt.trans_le` `LE.le.trans` `LT.lt.le` `toZ_neg` `toZ_nonneg` `IsPredArchimedean.exists_pred_iterate_of_le` `LinearOrder.isPredArchimedean_of_isSuccArchimedean` `iterate_pred_toZ` `Order.min_of_le_pred` `Monotone.antitone_iterate_of_map_le` `Order.pred_mono` `Order.pred_le`
`toZ_neg` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`toZ`	—	`lt_of_le_of_ne` `IsPredArchimedean.exists_pred_iterate_of_le` `LinearOrder.isPredArchimedean_of_isSuccArchimedean` `LT.lt.le` `toZ_of_lt` `iterate_pred_toZ` `neg_zero`
`toZ_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`toZ`	—	`IsSuccArchimedean.exists_succ_iterate_of_le` `toZ_of_ge`
`toZ_of_eq` 📖	mathematical	—	`toZ`	—	`IsSuccArchimedean.exists_succ_iterate_of_le` `le_rfl` `toZ_of_ge` `le_antisymm` `Nat.find_le` `Function.iterate_zero` `zero_le` `Nat.instCanonicallyOrderedAdd`
`toZ_of_ge` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`toZ` `Nat.find` `Nat.iterate` `Order.succ` `LinearOrder.toDecidableEq` `IsSuccArchimedean.exists_succ_iterate_of_le`	—	—
`toZ_of_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`toZ` `Nat.find` `Nat.iterate` `Order.pred` `LinearOrder.toDecidableEq` `IsPredArchimedean.exists_pred_iterate_of_le` `LinearOrder.isPredArchimedean_of_isSuccArchimedean` `LT.lt.le`	—	`not_le`

---

← Back to Index