# Documentation

Mathlib.Order.SuccPred.LinearLocallyFinite

# 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, ∞).

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

Instances For
theorem toZ_of_ge {ι : Type u_1} [] [] [] {i0 : ι} {i : ι} (hi : i0 i) :
toZ i0 i = ↑(Nat.find (_ : n, = i))
theorem toZ_of_lt {ι : Type u_1} [] [] [] {i0 : ι} {i : ι} (hi : i < i0) :
toZ i0 i = -↑(Nat.find (_ : n, = 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) :
theorem iterate_pred_toZ {ι : Type u_1} [] [] [] {i0 : ι} (i : ι) (hi : i < i0) :
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 () n
theorem toZ_iterate_pred_ge {ι : Type u_1} [] [] [] {i0 : ι} (n : ) :
-n toZ i0 ()
theorem toZ_iterate_succ_of_not_isMax {ι : Type u_1} [] [] [] {i0 : ι} (n : ) (hn : ¬IsMax ()) :
toZ i0 () = n
theorem toZ_iterate_pred_of_not_isMin {ι : Type u_1} [] [] [] {i0 : ι} (n : ) (hn : ¬IsMin ()) :
toZ 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 () = n
theorem toZ_iterate_pred {ι : Type u_1} [] [] [] {i0 : ι} [] (n : ) :
toZ i0 () = -n
theorem injective_toZ {ι : Type u_1} [] [] [] {i0 : ι} :
noncomputable def orderIsoRangeToZOfLinearSuccPredArch {ι : Type u_1} [] [] [] [hι : ] :
ι ≃o ↑(Set.range (toZ ()))

toZ defines an OrderIso between ι and its range.

Instances For
instance countable_of_linear_succ_pred_arch {ι : Type u_1} [] [] [] :
noncomputable def orderIsoIntOfLinearSuccPredArch {ι : Type u_1} [] [] [] [] [] [hι : ] :

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

Instances For
def orderIsoNatOfLinearSuccPredArch {ι : Type u_1} [] [] [] [] [] :

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

Instances For
def orderIsoRangeOfLinearSuccPredArch {ι : Type u_1} [] [] [] [] [] :
ι ≃o { x // x Finset.range (Int.toNat () + 1) }

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

Instances For