Linear locally finite orders

We prove that a LinearOrder which is a LocallyFiniteOrder also verifies

• SuccOrder
• PredOrder
• IsSuccArchimedean
• IsPredArchimedean
• Countable

Furthermore, we show that there is an OrderIso between such an order and a subset of ℤ.

Main definitions

• toZ i0 i: in a linear order on which we can define predecessors and successors and which is succ-archimedean, we can assign a unique integer toZ i0 i to each element i : ι while respecting the order, starting from toZ i0 i0 = 0.

Main results

Instances about linear locally finite orders:

• LinearLocallyFiniteOrder.SuccOrder: a linear locally finite order has a successor function.
• LinearLocallyFiniteOrder.PredOrder: a linear locally finite order has a predecessor function.
• LinearLocallyFiniteOrder.isSuccArchimedean: a linear locally finite order is succ-archimedean.
• LinearOrder.pred_archimedean_of_succ_archimedean: a succ-archimedean linear order is also pred-archimedean.
• countable_of_linear_succ_pred_arch : a succ-archimedean linear order is countable.

About toZ:

• orderIsoRangeToZOfLinearSuccPredArch: toZ defines an OrderIso between ι and its range.
• orderIsoNatOfLinearSuccPredArch: if the order has a bot but no top, toZ defines an OrderIso between ι and ℕ.
• orderIsoIntOfLinearSuccPredArch: if the order has neither bot nor top, toZ defines an OrderIso between ι and ℤ.
• orderIsoRangeOfLinearSuccPredArch: if the order has both a bot and a top, toZ gives an OrderIso between ι and Finset.range ((toZ ⊥ ⊤).toNat + 1).

noncomputable def LinearLocallyFiniteOrder.succFn {ι : Type u_1} [LinearOrder ι] (i : ι) : ι

Successor in a linear order. This defines a true successor only when i is isolated from above, i.e. when i is not the greatest lower bound of (i, ∞).

Equations

• LinearLocallyFiniteOrder.succFn i = Exists.choose (_ : ∃ (j : ι), IsGLB (Set.Ioi i) j)

theorem LinearLocallyFiniteOrder.succFn_spec {ι : Type u_1} [LinearOrder ι] (i : ι) : IsGLB (Set.Ioi i) (LinearLocallyFiniteOrder.succFn i)

theorem LinearLocallyFiniteOrder.le_succFn {ι : Type u_1} [LinearOrder ι] (i : ι) : i ≤ LinearLocallyFiniteOrder.succFn i

theorem LinearLocallyFiniteOrder.isGLB_Ioc_of_isGLB_Ioi {ι : Type u_1} [LinearOrder ι] {i : ι} {j : ι} {k : ι} (hij_lt : i < j) (h : IsGLB (Set.Ioi i) k) : IsGLB (Set.Ioc i j) k

theorem LinearLocallyFiniteOrder.isMax_of_succFn_le {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] (i : ι) (hi : LinearLocallyFiniteOrder.succFn i ≤ i) : IsMax i

theorem LinearLocallyFiniteOrder.succFn_le_of_lt {ι : Type u_1} [LinearOrder ι] (i : ι) (j : ι) (hij : i < j) : LinearLocallyFiniteOrder.succFn i ≤ j

theorem LinearLocallyFiniteOrder.le_of_lt_succFn {ι : Type u_1} [LinearOrder ι] (j : ι) (i : ι) (hij : j < LinearLocallyFiniteOrder.succFn i) : j ≤ i

noncomputable instance LinearLocallyFiniteOrder.instSuccOrderToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] : SuccOrder ι

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance LinearLocallyFiniteOrder.instPredOrderToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] : PredOrder ι

Equations

• LinearLocallyFiniteOrder.instPredOrderToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice = inferInstance

instance LinearLocallyFiniteOrder.isSuccArchimedean {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] : IsSuccArchimedean ι

Equations

• (_ : IsSuccArchimedean ι) = (_ : IsSuccArchimedean ι)

instance LinearOrder.isPredArchimedean_of_isSuccArchimedean {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] : IsPredArchimedean ι

Equations

• (_ : IsPredArchimedean ι) = (_ : IsPredArchimedean ι)

def toZ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] (i0 : ι) (i : ι) : ℤ

toZ numbers elements of ι according to their order, starting from i0. We prove in orderIsoRangeToZOfLinearSuccPredArch that this defines an OrderIso between ι and the range of toZ.

Equations

• toZ i0 i = if hi : i0 ≤ i then ↑(Nat.find (_ : ∃ (n : ℕ), Order.succ^[n] i0 = i)) else -↑(Nat.find (_ : ∃ (n : ℕ), Order.pred^[n] i0 = i))

theorem toZ_of_ge {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} {i : ι} (hi : i0 ≤ i) : toZ i0 i = ↑(Nat.find (_ : ∃ (n : ℕ), Order.succ^[n] i0 = i))

theorem toZ_of_lt {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} {i : ι} (hi : i < i0) : toZ i0 i = -↑(Nat.find (_ : ∃ (n : ℕ), Order.pred^[n] i0 = i))

@[simp]

theorem toZ_of_eq {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} : toZ i0 i0 = 0

theorem iterate_succ_toZ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (i : ι) (hi : i0 ≤ i) : Order.succ^[Int.toNat (toZ i0 i)] i0 = i

theorem iterate_pred_toZ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (i : ι) (hi : i < i0) : Order.pred^[Int.toNat (-toZ i0 i)] i0 = i

theorem toZ_nonneg {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} {i : ι} (hi : i0 ≤ i) : 0 ≤ toZ i0 i

theorem toZ_neg {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} {i : ι} (hi : i < i0) : toZ i0 i < 0

theorem toZ_iterate_succ_le {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (n : ℕ) : toZ i0 (Order.succ^[n] i0) ≤ ↑n

theorem toZ_iterate_pred_ge {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (n : ℕ) : -↑n ≤ toZ i0 (Order.pred^[n] i0)

theorem toZ_iterate_succ_of_not_isMax {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (n : ℕ) (hn : ¬IsMax (Order.succ^[n] i0)) : toZ i0 (Order.succ^[n] i0) = ↑n

theorem toZ_iterate_pred_of_not_isMin {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (n : ℕ) (hn : ¬IsMin (Order.pred^[n] i0)) : toZ i0 (Order.pred^[n] i0) = -↑n

theorem le_of_toZ_le {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} {i : ι} {j : ι} (h_le : toZ i0 i ≤ toZ i0 j) : i ≤ j

theorem toZ_mono {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} {i : ι} {j : ι} (h_le : i ≤ j) : toZ i0 i ≤ toZ i0 j

theorem toZ_le_iff {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (i : ι) (j : ι) : toZ i0 i ≤ toZ i0 j ↔ i ≤ j

theorem toZ_iterate_succ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} [NoMaxOrder ι] (n : ℕ) : toZ i0 (Order.succ^[n] i0) = ↑n

theorem toZ_iterate_pred {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} [NoMinOrder ι] (n : ℕ) : toZ i0 (Order.pred^[n] i0) = -↑n

theorem injective_toZ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} : Function.Injective (toZ i0)

noncomputable def orderIsoRangeToZOfLinearSuccPredArch {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] [hι : Nonempty ι] : ι ≃o ↑(Set.range (toZ (Nonempty.some hι)))

toZ defines an OrderIso between ι and its range.

Equations

• One or more equations did not get rendered due to their size.

instance countable_of_linear_succ_pred_arch {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] : Countable ι

Equations

• (_ : Countable ι) = (_ : Countable ι)

noncomputable def orderIsoIntOfLinearSuccPredArch {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] [NoMaxOrder ι] [NoMinOrder ι] [hι : Nonempty ι] : ι ≃o ℤ

If the order has neither bot nor top, toZ defines an OrderIso between ι and ℤ.

Equations

• One or more equations did not get rendered due to their size.

def orderIsoNatOfLinearSuccPredArch {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] [NoMaxOrder ι] [OrderBot ι] : ι ≃o ℕ

If the order has a bot but no top, toZ defines an OrderIso between ι and ℕ.

Equations

• One or more equations did not get rendered due to their size.

def orderIsoRangeOfLinearSuccPredArch {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] [OrderBot ι] [OrderTop ι] : ι ≃o { x : ℕ // x ∈ Finset.range (Int.toNat (toZ ⊥ ⊤) + 1) }

If the order has both a bot and a top, toZ gives an OrderIso between ι and Finset.range n for some n.

Equations

• One or more equations did not get rendered due to their size.