# 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)`.

source
@[instance 100]
instance LinearOrder.isPredArchimedean_of_isSuccArchimedean {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] :
IsPredArchimedean ι
source
instance LinearOrder.isSuccArchimedean_of_isPredArchimedean {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsPredArchimedean ι] :
IsSuccArchimedean ι
source
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.

source
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

Instances For

source
theorem LinearLocallyFiniteOrder.succFn_spec {ι : Type u_1} [LinearOrder ι] (i : ι) :
IsGLB (Set.Ioi i) (succFn i)
source
theorem LinearLocallyFiniteOrder.le_succFn {ι : Type u_1} [LinearOrder ι] (i : ι) :
i ≤ succFn i
source
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
source
theorem LinearLocallyFiniteOrder.isMax_of_succFn_le {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] (i : ι) (hi : succFn i ≤ i) :
IsMax i
source
theorem LinearLocallyFiniteOrder.succFn_le_of_lt {ι : Type u_1} [LinearOrder ι] (i j : ι) (hij : i < j) :
succFn i ≤ j
source
theorem LinearLocallyFiniteOrder.le_of_lt_succFn {ι : Type u_1} [LinearOrder ι] (j i : ι) (hij : j < succFn i) :
j ≤ i
source
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 := ⋯ }

Instances For

source
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 ι ᵒᵈ ᵒᵈ)

Instances For

source
@[instance 100]
instance LinearLocallyFiniteOrder.instIsSuccArchimedeanOfLocallyFiniteOrder {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [SuccOrder ι] :
IsSuccArchimedean ι
source
@[instance 100]
instance LinearLocallyFiniteOrder.instIsPredArchimedeanOfLocallyFiniteOrder {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [PredOrder ι] :
IsPredArchimedean ι
source
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 ⋯)

Instances For

source
theorem toZ_of_ge {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 i : ι} (hi : i0 ≤ i) :
toZ i0 i = ↑(Nat.find ⋯)
source
theorem toZ_of_lt {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 i : ι} (hi : i < i0) :
toZ i0 i = -↑(Nat.find ⋯)
source
@[simp]
theorem toZ_of_eq {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} :
toZ i0 i0 = 0
source
theorem iterate_succ_toZ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (i : ι) (hi : i0 ≤ i) :
Order.succ^[(toZ i0 i).toNat] i0 = i
source
theorem iterate_pred_toZ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (i : ι) (hi : i < i0) :
Order.pred^[(-toZ i0 i).toNat] i0 = i
source
theorem toZ_nonneg {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 i : ι} (hi : i0 ≤ i) :
0 ≤ toZ i0 i
source
theorem toZ_neg {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 i : ι} (hi : i < i0) :
toZ i0 i < 0
source
theorem toZ_iterate_succ_le {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (n : ℕ) :
toZ i0 (Order.succ^[n] i0) ≤ ↑n
source
theorem toZ_iterate_pred_ge {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (n : ℕ) :
-↑n ≤ toZ i0 (Order.pred^[n] i0)
source
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
source
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
source
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
source
theorem toZ_mono {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 i j : ι} (h_le : i ≤ j) :
toZ i0 i ≤ toZ i0 j
source
theorem toZ_le_iff {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (i j : ι) :
toZ i0 i ≤ toZ i0 j ↔ i ≤ j
source
theorem toZ_iterate_succ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} [NoMaxOrder ι] (n : ℕ) :
toZ i0 (Order.succ^[n] i0) = ↑n
source
theorem toZ_iterate_pred {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} [NoMinOrder ι] (n : ℕ) :
toZ i0 (Order.pred^[n] i0) = -↑n
source
theorem injective_toZ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} :
Function.Injective (toZ i0)
source
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' := ⋯ }

Instances For

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

Instances For

source
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' := ⋯ }

Instances For

source
def orderIsoRangeOfLinearSuccPredArch {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] [OrderBot ι] [OrderTop ι] :
ι ≃o ↥(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.

Instances For

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