# 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} [] (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
• = .choose
Instances For
theorem LinearLocallyFiniteOrder.succFn_spec {ι : Type u_1} [] (i : ι) :
theorem LinearLocallyFiniteOrder.le_succFn {ι : Type u_1} [] (i : ι) :
theorem LinearLocallyFiniteOrder.isGLB_Ioc_of_isGLB_Ioi {ι : Type u_1} [] {i : ι} {j : ι} {k : ι} (hij_lt : i < j) (h : IsGLB () k) :
IsGLB (Set.Ioc i j) k
theorem LinearLocallyFiniteOrder.isMax_of_succFn_le {ι : Type u_1} [] (i : ι) (hi : ) :
theorem LinearLocallyFiniteOrder.succFn_le_of_lt {ι : Type u_1} [] (i : ι) (j : ι) (hij : i < j) :
theorem LinearLocallyFiniteOrder.le_of_lt_succFn {ι : Type u_1} [] (j : ι) (i : ι) (hij : ) :
j i
@[instance 100]
Equations
• LinearLocallyFiniteOrder.instSuccOrderOfLocallyFiniteOrder = { succ := LinearLocallyFiniteOrder.succFn, le_succ := , max_of_succ_le := , succ_le_of_lt := , le_of_lt_succ := }
@[instance 100]
Equations
• LinearLocallyFiniteOrder.instPredOrderOfLocallyFiniteOrder = inferInstance
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
def toZ {ι : Type u_1} [] [] [] (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 () else -()
Instances For
theorem toZ_of_ge {ι : Type u_1} [] [] [] {i0 : ι} {i : ι} (hi : i0 i) :
toZ i0 i = ()
theorem toZ_of_lt {ι : Type u_1} [] [] [] {i0 : ι} {i : ι} (hi : i < i0) :
toZ i0 i = -()
@[simp]
theorem toZ_of_eq {ι : Type u_1} [] [] [] {i0 : ι} :
toZ i0 i0 = 0
theorem iterate_succ_toZ {ι : Type u_1} [] [] [] {i0 : ι} (i : ι) (hi : i0 i) :
Order.succ^[(toZ i0 i).toNat] i0 = i
theorem iterate_pred_toZ {ι : Type u_1} [] [] [] {i0 : ι} (i : ι) (hi : i < i0) :
Order.pred^[(-toZ i0 i).toNat] i0 = i
theorem toZ_nonneg {ι : Type u_1} [] [] [] {i0 : ι} {i : ι} (hi : i0 i) :
0 toZ i0 i
theorem toZ_neg {ι : Type u_1} [] [] [] {i0 : ι} {i : ι} (hi : i < i0) :
toZ i0 i < 0
theorem toZ_iterate_succ_le {ι : Type u_1} [] [] [] {i0 : ι} (n : ) :
toZ i0 (Order.succ^[n] i0) n
theorem toZ_iterate_pred_ge {ι : Type u_1} [] [] [] {i0 : ι} (n : ) :
-n toZ i0 (Order.pred^[n] i0)
theorem toZ_iterate_succ_of_not_isMax {ι : Type u_1} [] [] [] {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} [] [] [] {i0 : ι} (n : ) (hn : ¬IsMin (Order.pred^[n] i0)) :
toZ i0 (Order.pred^[n] i0) = -n
theorem le_of_toZ_le {ι : Type u_1} [] [] [] {i0 : ι} {i : ι} {j : ι} (h_le : toZ i0 i toZ i0 j) :
i j
theorem toZ_mono {ι : Type u_1} [] [] [] {i0 : ι} {i : ι} {j : ι} (h_le : i j) :
toZ i0 i toZ i0 j
theorem toZ_le_iff {ι : Type u_1} [] [] [] {i0 : ι} (i : ι) (j : ι) :
toZ i0 i toZ i0 j i j
theorem toZ_iterate_succ {ι : Type u_1} [] [] [] {i0 : ι} [] (n : ) :
toZ i0 (Order.succ^[n] i0) = n
theorem toZ_iterate_pred {ι : Type u_1} [] [] [] {i0 : ι} [] (n : ) :
toZ i0 (Order.pred^[n] i0) = -n
theorem injective_toZ {ι : Type u_1} [] [] [] {i0 : ι} :
noncomputable def orderIsoRangeToZOfLinearSuccPredArch {ι : Type u_1} [] [] [] [hι : ] :
ι ≃o (Set.range (toZ .some))

toZ defines an OrderIso between ι and its range.

Equations
• orderIsoRangeToZOfLinearSuccPredArch = { toEquiv := Equiv.ofInjective (toZ .some) , map_rel_iff' := }
Instances For
@[instance 100]
instance countable_of_linear_succ_pred_arch {ι : Type u_1} [] [] [] :
Equations
• =
noncomputable def orderIsoIntOfLinearSuccPredArch {ι : Type u_1} [] [] [] [] [] [hι : ] :

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.
Instances For
def orderIsoNatOfLinearSuccPredArch {ι : Type u_1} [] [] [] [] [] :

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' := }
Instances For
def orderIsoRangeOfLinearSuccPredArch {ι : Type u_1} [] [] [] [] [] :
ι ≃o { x : // x Finset.range (().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.
Instances For