Documentation

Mathlib.Order.SuccPred.LinearLocallyFinite

Linear locally finite orders #

We prove that a LinearOrder which is a LocallyFiniteOrder also verifies

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

Main definitions #

Main results #

Instances about linear locally finite orders:

About toZ:

@[instance 100]
Equations
  • =
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
Instances For
    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
    theorem LinearLocallyFiniteOrder.succFn_le_of_lt {ι : Type u_1} [LinearOrder ι] (i : ι) (j : ι) (hij : i < j) :
    theorem LinearLocallyFiniteOrder.le_of_lt_succFn {ι : Type u_1} [LinearOrder ι] (j : ι) (i : ι) (hij : j < LinearLocallyFiniteOrder.succFn i) :
    j i
    @[instance 100]
    Equations
    • LinearLocallyFiniteOrder.instSuccOrderOfLocallyFiniteOrder = { succ := LinearLocallyFiniteOrder.succFn, le_succ := , max_of_succ_le := , succ_le_of_lt := }
    @[instance 100]
    Equations
    @[instance 100]
    Equations
    • =
    @[instance 100]
    Equations
    • =
    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
    Instances For
      theorem toZ_of_ge {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} {i : ι} (hi : i0 i) :
      toZ i0 i = (Nat.find )
      theorem toZ_of_lt {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} {i : ι} (hi : i < i0) :
      toZ i0 i = -(Nat.find )
      @[simp]
      theorem toZ_of_eq {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} :
      toZ i0 i0 = 0
      theorem iterate_succ_toZ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (i : ι) (hi : i0 i) :
      Order.succ^[(toZ i0 i).toNat] i0 = i
      theorem iterate_pred_toZ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (i : ι) (hi : i < i0) :
      Order.pred^[(-toZ i0 i).toNat] i0 = i
      theorem toZ_nonneg {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} {i : ι} (hi : i0 i) :
      0 toZ i0 i
      theorem toZ_neg {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} {i : ι} (hi : i < i0) :
      toZ i0 i < 0
      theorem toZ_iterate_succ_le {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (n : ) :
      toZ i0 (Order.succ^[n] i0) n
      theorem toZ_iterate_pred_ge {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (n : ) :
      -n toZ i0 (Order.pred^[n] i0)
      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
      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
      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
      theorem toZ_mono {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} {i : ι} {j : ι} (h_le : i j) :
      toZ i0 i toZ i0 j
      theorem toZ_le_iff {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} (i : ι) (j : ι) :
      toZ i0 i toZ i0 j i j
      theorem toZ_iterate_succ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} [NoMaxOrder ι] (n : ) :
      toZ i0 (Order.succ^[n] i0) = n
      theorem toZ_iterate_pred {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} [NoMinOrder ι] (n : ) :
      toZ i0 (Order.pred^[n] i0) = -n
      theorem injective_toZ {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 : ι} :
      noncomputable def orderIsoRangeToZOfLinearSuccPredArch {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] [hι : Nonempty ι] :
      ι ≃o (Set.range (toZ .some))

      toZ defines an OrderIso between ι and its range.

      Equations
      • orderIsoRangeToZOfLinearSuccPredArch = { toEquiv := Equiv.ofInjective (toZ .some) , map_rel_iff' := }
      Instances For
        @[instance 100]
        Equations
        • =
        noncomputable def orderIsoIntOfLinearSuccPredArch {ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] [NoMaxOrder ι] [NoMinOrder ι] [hι : Nonempty ι] :

        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

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