# mathlib3documentation

order.succ_pred.linear_locally_finite

# Linear locally finite orders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We prove that a linear_order which is a locally_finite_order also verifies

• succ_order
• pred_order
• is_succ_archimedean
• is_pred_archimedean
• countable

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

## Main definitions #

• to_Z 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 to_Z i0 i to each element i : ι while respecting the order, starting from to_Z i0 i0 = 0.

## Main results #

Instances about linear locally finite orders:

• linear_locally_finite_order.succ_order: a linear locally finite order has a successor function.
• linear_locally_finite_order.pred_order: a linear locally finite order has a predecessor function.
• linear_locally_finite_order.is_succ_archimedean: a linear locally finite order is succ-archimedean.
• linear_order.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 to_Z:

• order_iso_range_to_Z_of_linear_succ_pred_arch: to_Z defines an order_iso between ι and its range.
• order_iso_nat_of_linear_succ_pred_arch: if the order has a bot but no top, to_Z defines an order_iso between ι and ℕ.
• order_iso_int_of_linear_succ_pred_arch: if the order has neither bot nor top, to_Z defines an order_iso between ι and ℤ.
• order_iso_range_of_linear_succ_pred_arch: if the order has both a bot and a top, to_Z gives an order_iso between ι and finset.range ((to_Z ⊥ ⊤).to_nat + 1).
noncomputable def linear_locally_finite_order.succ_fn {ι : Type u_1} [linear_order ι] (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
theorem linear_locally_finite_order.le_succ_fn {ι : Type u_1} [linear_order ι] (i : ι) :
theorem linear_locally_finite_order.is_glb_Ioc_of_is_glb_Ioi {ι : Type u_1} [linear_order ι] {i j k : ι} (hij_lt : i < j) (h : is_glb (set.Ioi i) k) :
is_glb (set.Ioc i j) k
theorem linear_locally_finite_order.is_max_of_succ_fn_le {ι : Type u_1} [linear_order ι] (i : ι) (hi : i) :
theorem linear_locally_finite_order.succ_fn_le_of_lt {ι : Type u_1} [linear_order ι] (i j : ι) (hij : i < j) :
theorem linear_locally_finite_order.le_of_lt_succ_fn {ι : Type u_1} [linear_order ι] (j i : ι) (hij : j < ) :
j i
@[protected, instance]
noncomputable def linear_locally_finite_order.succ_order {ι : Type u_1} [linear_order ι]  :
Equations
@[protected, instance]
noncomputable def linear_locally_finite_order.pred_order {ι : Type u_1} [linear_order ι]  :
Equations
@[protected, instance]
@[protected, instance]
def to_Z {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] (i0 i : ι) :

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

Equations
theorem to_Z_of_ge {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 i : ι} (hi : i0 i) :
to_Z i0 i = (nat.find _)
theorem to_Z_of_lt {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 i : ι} (hi : i < i0) :
@[simp]
theorem to_Z_of_eq {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 : ι} :
to_Z i0 i0 = 0
theorem iterate_succ_to_Z {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 : ι} (i : ι) (hi : i0 i) :
theorem iterate_pred_to_Z {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 : ι} (i : ι) (hi : i < i0) :
theorem to_Z_nonneg {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 i : ι} (hi : i0 i) :
0 to_Z i0 i
theorem to_Z_neg {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 i : ι} (hi : i < i0) :
to_Z i0 i < 0
theorem to_Z_iterate_succ_le {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 : ι} (n : ) :
theorem to_Z_iterate_pred_ge {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 : ι} (n : ) :
theorem to_Z_iterate_succ_of_not_is_max {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 : ι} (n : ) (hn : ¬is_max (order.succ^[n] i0)) :
theorem to_Z_iterate_pred_of_not_is_min {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 : ι} (n : ) (hn : ¬is_min (order.pred^[n] i0)) :
theorem le_of_to_Z_le {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 i j : ι} (h_le : to_Z i0 i to_Z i0 j) :
i j
theorem to_Z_mono {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 i j : ι} (h_le : i j) :
to_Z i0 i to_Z i0 j
theorem to_Z_le_iff {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 : ι} (i j : ι) :
to_Z i0 i to_Z i0 j i j
theorem to_Z_iterate_succ {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 : ι} [no_max_order ι] (n : ) :
theorem to_Z_iterate_pred {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 : ι} [no_min_order ι] (n : ) :
theorem injective_to_Z {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] {i0 : ι} :
noncomputable def order_iso_range_to_Z_of_linear_succ_pred_arch {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] [hι : nonempty ι] :

to_Z defines an order_iso between ι and its range.

Equations
@[protected, instance]
noncomputable def order_iso_int_of_linear_succ_pred_arch {ι : Type u_1} [linear_order ι] [succ_order ι] [pred_order ι] [no_max_order ι] [no_min_order ι] [hι : nonempty ι] :

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

Equations

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

Equations

If the order has both a bot and a top, to_Z gives an order_iso between ι and finset.range n for some n.

Equations