mathlib3 documentation

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

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

Main definitions #

Main results #

Instances about linear locally finite orders:

About to_Z:

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.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
def to_Z {ι : Type u_1} [linear_order ι] [succ_order ι] [is_succ_archimedean ι] [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 ι] [is_succ_archimedean ι] [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 ι] [is_succ_archimedean ι] [pred_order ι] {i0 i : ι} (hi : i < i0) :
@[simp]
theorem to_Z_of_eq {ι : Type u_1} [linear_order ι] [succ_order ι] [is_succ_archimedean ι] [pred_order ι] {i0 : ι} :
to_Z i0 i0 = 0
theorem iterate_succ_to_Z {ι : Type u_1} [linear_order ι] [succ_order ι] [is_succ_archimedean ι] [pred_order ι] {i0 : ι} (i : ι) (hi : i0 i) :
theorem iterate_pred_to_Z {ι : Type u_1} [linear_order ι] [succ_order ι] [is_succ_archimedean ι] [pred_order ι] {i0 : ι} (i : ι) (hi : i < i0) :
theorem to_Z_nonneg {ι : Type u_1} [linear_order ι] [succ_order ι] [is_succ_archimedean ι] [pred_order ι] {i0 i : ι} (hi : i0 i) :
0 to_Z i0 i
theorem to_Z_neg {ι : Type u_1} [linear_order ι] [succ_order ι] [is_succ_archimedean ι] [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 ι] [is_succ_archimedean ι] [pred_order ι] {i0 : ι} (n : ) :
theorem to_Z_iterate_pred_ge {ι : Type u_1} [linear_order ι] [succ_order ι] [is_succ_archimedean ι] [pred_order ι] {i0 : ι} (n : ) :
theorem to_Z_iterate_succ_of_not_is_max {ι : Type u_1} [linear_order ι] [succ_order ι] [is_succ_archimedean ι] [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 ι] [is_succ_archimedean ι] [pred_order ι] {i0 : ι} (n : ) (hn : ¬is_min (order.pred^[n] i0)) :
theorem le_of_to_Z_le {ι : Type u_1} [linear_order ι] [succ_order ι] [is_succ_archimedean ι] [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 ι] [is_succ_archimedean ι] [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 ι] [is_succ_archimedean ι] [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 ι] [is_succ_archimedean ι] [pred_order ι] {i0 : ι} [no_max_order ι] (n : ) :
theorem to_Z_iterate_pred {ι : Type u_1} [linear_order ι] [succ_order ι] [is_succ_archimedean ι] [pred_order ι] {i0 : ι} [no_min_order ι] (n : ) :
theorem injective_to_Z {ι : Type u_1} [linear_order ι] [succ_order ι] [is_succ_archimedean ι] [pred_order ι] {i0 : ι} :

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 ι] [is_succ_archimedean ι] [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