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

Results 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).

@[instance 100]

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

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

theorem LinearOrder.isSuccArchimedean_iff_isPredArchimedean {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] : IsSuccArchimedean ι ↔ IsPredArchimedean ι

In a linear SuccOrder that's also a PredOrder, IsSuccArchimedean and IsPredArchimedean are equivalent.

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 = ⋯.choose

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 def LinearLocallyFiniteOrder.succOrder (ι : Type u_1) [LinearOrder ι] [LocallyFiniteOrder ι] : SuccOrder ι

A locally finite order is a SuccOrder. This is not an instance, because its succ field conflicts with computable SuccOrder structures on ℕ and ℤ.

Equations

• LinearLocallyFiniteOrder.succOrder ι = { succ := LinearLocallyFiniteOrder.succFn, le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }

noncomputable def LinearLocallyFiniteOrder.predOrder (ι : Type u_1) [LinearOrder ι] [LocallyFiniteOrder ι] : PredOrder ι

A locally finite order is a PredOrder. This is not an instance, because its succ field conflicts with computable PredOrder structures on ℕ and ℤ.

Equations

• LinearLocallyFiniteOrder.predOrder ι = inferInstanceAs (PredOrder ιᵒᵈᵒᵈ)

@[instance 100]

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

@[instance 100]

instance LinearLocallyFiniteOrder.instIsPredArchimedeanOfLocallyFiniteOrder {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [PredOrder ι] : 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 ⋯) else -↑(Nat.find ⋯)

theorem toZ_of_ge {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 i : ι} (hi : i0 ≤ i) : toZ i0 i = ↑(Nat.find ⋯)

theorem toZ_of_lt {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 i : ι} (hi : i < i0) : toZ i0 i = -↑(Nat.find ⋯)

@[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^[(toZ i0 i).toNat] i0 = i

theorem iterate_pred_toZ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (i : ι) (hi : i < i0) : Order.pred^[(-toZ i0 i).toNat] 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 hι.some))

toZ defines an OrderIso between ι and its range.

Equations

• orderIsoRangeToZOfLinearSuccPredArch = { toEquiv := Equiv.ofInjective (toZ hι.some) ⋯, map_rel_iff' := ⋯ }

@[instance 100]

instance countable_of_linear_succ_pred_arch {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] : 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

• orderIsoNatOfLinearSuccPredArch = { toFun := fun (i : ι) => (toZ ⊥ i).toNat, invFun := fun (n : ℕ) => Order.succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

def orderIsoRangeOfLinearSuccPredArch {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] [OrderBot ι] [OrderTop ι] : ι ≃o { x : ℕ // x ∈ Finset.range ((toZ ⊥ ⊤).toNat + 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.

@[instance 100]

instance Countable.of_linearOrder_locallyFiniteOrder {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] : Countable ι