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 #
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 integerto_Z i0 ito each elementi : ιwhile respecting the order, starting fromto_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_Zdefines anorder_isobetweenιand its range.order_iso_nat_of_linear_succ_pred_arch: if the order has a bot but no top,to_Zdefines anorder_isobetweenιandℕ.order_iso_int_of_linear_succ_pred_arch: if the order has neither bot nor top,to_Zdefines anorder_isobetweenιandℤ.order_iso_range_of_linear_succ_pred_arch: if the order has both a bot and a top,to_Zgives anorder_isobetweenιandfinset.range ((to_Z ⊥ ⊤).to_nat + 1).
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) :
theorem
linear_locally_finite_order.is_max_of_succ_fn_le
{ι : Type u_1}
[linear_order ι]
[locally_finite_order ι]
(i : ι)
(hi : linear_locally_finite_order.succ_fn i ≤ i) :
is_max 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 < linear_locally_finite_order.succ_fn i) :
j ≤ i
@[protected, instance]
noncomputable
def
linear_locally_finite_order.succ_order
{ι : Type u_1}
[linear_order ι]
[locally_finite_order ι] :
Equations
- linear_locally_finite_order.succ_order = {succ := linear_locally_finite_order.succ_fn _inst_1, le_succ := _, max_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}
@[protected, instance]
noncomputable
def
linear_locally_finite_order.pred_order
{ι : Type u_1}
[linear_order ι]
[locally_finite_order ι] :
@[protected, instance]
def
linear_locally_finite_order.is_succ_archimedean
{ι : Type u_1}
[linear_order ι]
[locally_finite_order ι] :
@[protected, instance]
def
linear_order.pred_archimedean_of_succ_archimedean
{ι : Type u_1}
[linear_order ι]
[succ_order ι]
[pred_order ι]
[is_succ_archimedean ι] :
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.
theorem
to_Z_of_ge
{ι : Type u_1}
[linear_order ι]
[succ_order ι]
[is_succ_archimedean ι]
[pred_order ι]
{i0 i : ι}
(hi : i0 ≤ i) :
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 : ι} :
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) :
theorem
to_Z_neg
{ι : Type u_1}
[linear_order ι]
[succ_order ι]
[is_succ_archimedean ι]
[pred_order ι]
{i0 i : ι}
(hi : i < i0) :
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) :
theorem
to_Z_le_iff
{ι : Type u_1}
[linear_order ι]
[succ_order ι]
[is_succ_archimedean ι]
[pred_order ι]
{i0 : ι}
(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 : ι} :
function.injective (to_Z i0)
noncomputable
def
order_iso_range_to_Z_of_linear_succ_pred_arch
{ι : Type u_1}
[linear_order ι]
[succ_order ι]
[pred_order ι]
[is_succ_archimedean ι]
[hι : nonempty ι] :
to_Z defines an order_iso between ι and its range.
Equations
- order_iso_range_to_Z_of_linear_succ_pred_arch = {to_equiv := equiv.of_injective (to_Z hι.some) order_iso_range_to_Z_of_linear_succ_pred_arch._proof_1, map_rel_iff' := _}
@[protected, instance]
def
countable_of_linear_succ_pred_arch
{ι : Type u_1}
[linear_order ι]
[succ_order ι]
[pred_order ι]
[is_succ_archimedean ι] :
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 ℤ.
def
order_iso_nat_of_linear_succ_pred_arch
{ι : Type u_1}
[linear_order ι]
[succ_order ι]
[pred_order ι]
[is_succ_archimedean ι]
[no_max_order ι]
[order_bot ι] :
If the order has a bot but no top, to_Z defines an order_iso between ι and ℕ.
def
order_iso_range_of_linear_succ_pred_arch
{ι : Type u_1}
[linear_order ι]
[succ_order ι]
[pred_order ι]
[is_succ_archimedean ι]
[order_bot ι]
[order_top ι] :
If the order has both a bot and a top, to_Z gives an order_iso between ι and
finset.range n for some n.