Documentation

Mathlib.Algebra.Order.SuccPred

Interaction between successors and arithmetic #

We define the SuccAddOrder and PredSubOrder typeclasses, for orders satisfying succ x = x + 1 and pred x = x - 1 respectively. This allows us to transfer the API for successors and predecessors into these common arithmetical forms.

Todo #

In the future, we will make x + 1 and x - 1 the simp-normal forms for succ x and pred x respectively. This will require a refactor of Ordinal first, as the simp-normal form is currently set the other way around.

class SuccAddOrder (α : Type u_1) [Preorder α] [Add α] [One α] extends SuccOrder α :
Type u_1

A typeclass for succ x = x + 1.

Instances
    class PredSubOrder (α : Type u_1) [Preorder α] [Sub α] [One α] extends PredOrder α :
    Type u_1

    A typeclass for pred x = x - 1.

    Instances
      theorem Order.succ_eq_add_one {α : Type u_1} [Preorder α] [Add α] [One α] [SuccAddOrder α] (x : α) :
      Order.succ x = x + 1
      theorem Order.add_one_le_of_lt {α : Type u_1} {x y : α} [Preorder α] [Add α] [One α] [SuccAddOrder α] (h : x < y) :
      x + 1 y
      theorem Order.add_one_le_iff_of_not_isMax {α : Type u_1} {x y : α} [Preorder α] [Add α] [One α] [SuccAddOrder α] (hx : ¬IsMax x) :
      x + 1 y x < y
      theorem Order.add_one_le_iff {α : Type u_1} {x y : α} [Preorder α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] :
      x + 1 y x < y
      @[simp]
      theorem Order.wcovBy_add_one {α : Type u_1} [Preorder α] [Add α] [One α] [SuccAddOrder α] (x : α) :
      x ⩿ x + 1
      @[simp]
      theorem Order.covBy_add_one {α : Type u_1} [Preorder α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] (x : α) :
      x x + 1
      theorem Order.pred_eq_sub_one {α : Type u_1} [Preorder α] [Sub α] [One α] [PredSubOrder α] (x : α) :
      Order.pred x = x - 1
      theorem Order.le_sub_one_of_lt {α : Type u_1} {x y : α} [Preorder α] [Sub α] [One α] [PredSubOrder α] (h : x < y) :
      x y - 1
      theorem Order.le_sub_one_iff_of_not_isMin {α : Type u_1} {x y : α} [Preorder α] [Sub α] [One α] [PredSubOrder α] (hy : ¬IsMin y) :
      x y - 1 x < y
      theorem Order.le_sub_one_iff {α : Type u_1} {x y : α} [Preorder α] [Sub α] [One α] [PredSubOrder α] [NoMinOrder α] :
      x y - 1 x < y
      @[simp]
      theorem Order.sub_one_wcovBy {α : Type u_1} [Preorder α] [Sub α] [One α] [PredSubOrder α] (x : α) :
      x - 1 ⩿ x
      @[simp]
      theorem Order.sub_one_covBy {α : Type u_1} [Preorder α] [Sub α] [One α] [PredSubOrder α] [NoMinOrder α] (x : α) :
      x - 1 x
      @[simp]
      theorem Order.succ_iterate {α : Type u_1} [Preorder α] [AddMonoidWithOne α] [SuccAddOrder α] (x : α) (n : ) :
      Order.succ^[n] x = x + n
      @[simp]
      theorem Order.pred_iterate {α : Type u_1} [Preorder α] [AddCommGroupWithOne α] [PredSubOrder α] (x : α) (n : ) :
      Order.pred^[n] x = x - n
      theorem Order.not_isMax_zero {α : Type u_1} [PartialOrder α] [Zero α] [One α] [ZeroLEOneClass α] [NeZero 1] :
      theorem Order.one_le_iff_pos {α : Type u_1} {x : α} [PartialOrder α] [AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero 1] [SuccAddOrder α] :
      1 x 0 < x
      theorem Order.covBy_iff_add_one_eq {α : Type u_1} {x y : α} [PartialOrder α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] :
      x y x + 1 = y
      theorem Order.covBy_iff_sub_one_eq {α : Type u_1} {x y : α} [PartialOrder α] [Sub α] [One α] [PredSubOrder α] [NoMinOrder α] :
      x y y - 1 = x
      theorem Order.IsSuccPrelimit.add_one_lt {α : Type u_1} {x y : α} [PartialOrder α] [Add α] [One α] [SuccAddOrder α] (hx : Order.IsSuccPrelimit x) (hy : y < x) :
      y + 1 < x
      theorem Order.IsPredPrelimit.lt_sub_one {α : Type u_1} {x y : α} [PartialOrder α] [Sub α] [One α] [PredSubOrder α] (hx : Order.IsPredPrelimit x) (hy : x < y) :
      x < y - 1
      theorem Order.IsSuccLimit.add_one_lt {α : Type u_1} {x y : α} [PartialOrder α] [Add α] [One α] [SuccAddOrder α] (hx : Order.IsSuccLimit x) (hy : y < x) :
      y + 1 < x
      theorem Order.IsPredLimit.lt_sub_one {α : Type u_1} {x y : α} [PartialOrder α] [Sub α] [One α] [PredSubOrder α] (hx : Order.IsPredLimit x) (hy : x < y) :
      x < y - 1
      theorem Order.IsSuccPrelimit.add_natCast_lt {α : Type u_1} {x y : α} [PartialOrder α] [AddMonoidWithOne α] [SuccAddOrder α] (hx : Order.IsSuccPrelimit x) (hy : y < x) (n : ) :
      y + n < x
      theorem Order.IsPredPrelimit.lt_sub_natCast {α : Type u_1} {x y : α} [PartialOrder α] [AddCommGroupWithOne α] [PredSubOrder α] (hx : Order.IsPredPrelimit x) (hy : x < y) (n : ) :
      x < y - n
      theorem Order.IsSuccLimit.add_natCast_lt {α : Type u_1} {x y : α} [PartialOrder α] [AddMonoidWithOne α] [SuccAddOrder α] (hx : Order.IsSuccLimit x) (hy : y < x) (n : ) :
      y + n < x
      theorem Order.IsPredLimit.lt_sub_natCast {α : Type u_1} {x y : α} [PartialOrder α] [AddCommGroupWithOne α] [PredSubOrder α] (hx : Order.IsPredLimit x) (hy : x < y) (n : ) :
      x < y - n
      theorem Order.le_of_lt_add_one {α : Type u_1} {x y : α} [LinearOrder α] [Add α] [One α] [SuccAddOrder α] (h : x < y + 1) :
      x y
      theorem Order.lt_add_one_iff_of_not_isMax {α : Type u_1} {x y : α} [LinearOrder α] [Add α] [One α] [SuccAddOrder α] (hy : ¬IsMax y) :
      x < y + 1 x y
      theorem Order.lt_add_one_iff {α : Type u_1} {x y : α} [LinearOrder α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] :
      x < y + 1 x y
      theorem Order.le_of_sub_one_lt {α : Type u_1} {x y : α} [LinearOrder α] [Sub α] [One α] [PredSubOrder α] (h : x - 1 < y) :
      x y
      theorem Order.sub_one_lt_iff_of_not_isMin {α : Type u_1} {x y : α} [LinearOrder α] [Sub α] [One α] [PredSubOrder α] (hx : ¬IsMin x) :
      x - 1 < y x y
      theorem Order.sub_one_lt_iff {α : Type u_1} {x y : α} [LinearOrder α] [Sub α] [One α] [PredSubOrder α] [NoMinOrder α] :
      x - 1 < y x y
      theorem Order.lt_one_iff_nonpos {α : Type u_1} {x : α} [LinearOrder α] [AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero 1] [SuccAddOrder α] :
      x < 1 x 0
      theorem monotoneOn_of_le_add_one {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Add α] [One α] [SuccAddOrder α] [IsSuccArchimedean α] {s : Set α} {f : αβ} (hs : s.OrdConnected) :
      (∀ (a : α), ¬IsMax aa sa + 1 sf a f (a + 1))MonotoneOn f s
      theorem antitoneOn_of_add_one_le {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Add α] [One α] [SuccAddOrder α] [IsSuccArchimedean α] {s : Set α} {f : αβ} (hs : s.OrdConnected) :
      (∀ (a : α), ¬IsMax aa sa + 1 sf (a + 1) f a)AntitoneOn f s
      theorem strictMonoOn_of_lt_add_one {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Add α] [One α] [SuccAddOrder α] [IsSuccArchimedean α] {s : Set α} {f : αβ} (hs : s.OrdConnected) :
      (∀ (a : α), ¬IsMax aa sa + 1 sf a < f (a + 1))StrictMonoOn f s
      theorem strictAntiOn_of_add_one_lt {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Add α] [One α] [SuccAddOrder α] [IsSuccArchimedean α] {s : Set α} {f : αβ} (hs : s.OrdConnected) :
      (∀ (a : α), ¬IsMax aa sa + 1 sf (a + 1) < f a)StrictAntiOn f s
      theorem monotone_of_le_add_one {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Add α] [One α] [SuccAddOrder α] [IsSuccArchimedean α] {f : αβ} :
      (∀ (a : α), ¬IsMax af a f (a + 1))Monotone f
      theorem antitone_of_add_one_le {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Add α] [One α] [SuccAddOrder α] [IsSuccArchimedean α] {f : αβ} :
      (∀ (a : α), ¬IsMax af (a + 1) f a)Antitone f
      theorem strictMono_of_lt_add_one {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Add α] [One α] [SuccAddOrder α] [IsSuccArchimedean α] {f : αβ} :
      (∀ (a : α), ¬IsMax af a < f (a + 1))StrictMono f
      theorem strictAnti_of_add_one_lt {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Add α] [One α] [SuccAddOrder α] [IsSuccArchimedean α] {f : αβ} :
      (∀ (a : α), ¬IsMax af (a + 1) < f a)StrictAnti f
      theorem monotoneOn_of_sub_one_le {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Sub α] [One α] [PredSubOrder α] [IsPredArchimedean α] {s : Set α} {f : αβ} (hs : s.OrdConnected) :
      (∀ (a : α), ¬IsMin aa sa - 1 sf (a - 1) f a)MonotoneOn f s
      theorem antitoneOn_of_le_sub_one {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Sub α] [One α] [PredSubOrder α] [IsPredArchimedean α] {s : Set α} {f : αβ} (hs : s.OrdConnected) :
      (∀ (a : α), ¬IsMin aa sa - 1 sf a f (a - 1))AntitoneOn f s
      theorem strictMonoOn_of_sub_one_lt {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Sub α] [One α] [PredSubOrder α] [IsPredArchimedean α] {s : Set α} {f : αβ} (hs : s.OrdConnected) :
      (∀ (a : α), ¬IsMin aa sa - 1 sf (a - 1) < f a)StrictMonoOn f s
      theorem strictAntiOn_of_lt_sub_one {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Sub α] [One α] [PredSubOrder α] [IsPredArchimedean α] {s : Set α} {f : αβ} (hs : s.OrdConnected) :
      (∀ (a : α), ¬IsMin aa sa - 1 sf a < f (a - 1))StrictAntiOn f s
      theorem monotone_of_sub_one_le {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Sub α] [One α] [PredSubOrder α] [IsPredArchimedean α] {f : αβ} :
      (∀ (a : α), ¬IsMin af (a - 1) f a)Monotone f
      theorem antitone_of_le_sub_one {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Sub α] [One α] [PredSubOrder α] [IsPredArchimedean α] {f : αβ} :
      (∀ (a : α), ¬IsMin af a f (a - 1))Antitone f
      theorem strictMono_of_sub_one_lt {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Sub α] [One α] [PredSubOrder α] [IsPredArchimedean α] {f : αβ} :
      (∀ (a : α), ¬IsMin af (a - 1) < f a)StrictMono f
      theorem strictAnti_of_lt_sub_one {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Sub α] [One α] [PredSubOrder α] [IsPredArchimedean α] {f : αβ} :
      (∀ (a : α), ¬IsMin af a < f (a - 1))StrictAnti f