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.

succ : α → α
le_succ (a : α) : a ≤ succ a
max_of_succ_le {a : α} : succ a ≤ a → IsMax a
succ_le_of_lt {a b : α} : a < b → succ a ≤ b
succ_eq_add_one (x : α) : SuccOrder.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.

pred : α → α
pred_le (a : α) : pred a ≤ a
min_of_le_pred {a : α} : a ≤ pred a → IsMin a
le_pred_of_lt {a b : α} : a < b → a ≤ pred b
pred_eq_sub_one (x : α) : PredOrder.pred x = x - 1

Instances

Nat.instPredSubOrder

theorem Order.succ_eq_add_one {α : Type u_1} [Preorder α] [Add α] [One α] [SuccAddOrder α] (x : α) :

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 : α) :

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 : ℕ) :

succ ^[n] x = x + ↑n

@[simp]

theorem Order.pred_iterate {α : Type u_1} [Preorder α] [AddCommGroupWithOne α] [PredSubOrder α] (x : α) (n : ℕ) :

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 : IsSuccPrelimit x) (hy : y < x) :

y + 1 < x

theorem Order.IsPredPrelimit.lt_sub_one {α : Type u_1} {x y : α} [PartialOrder α] [Sub α] [One α] [PredSubOrder α] (hx : IsPredPrelimit x) (hy : x < y) :

x < y - 1

theorem Order.IsSuccLimit.add_one_lt {α : Type u_1} {x y : α} [PartialOrder α] [Add α] [One α] [SuccAddOrder α] (hx : IsSuccLimit x) (hy : y < x) :

y + 1 < x

theorem Order.IsPredLimit.lt_sub_one {α : Type u_1} {x y : α} [PartialOrder α] [Sub α] [One α] [PredSubOrder α] (hx : IsPredLimit x) (hy : x < y) :

x < y - 1

theorem Order.IsSuccPrelimit.add_natCast_lt {α : Type u_1} {x y : α} [PartialOrder α] [AddMonoidWithOne α] [SuccAddOrder α] (hx : IsSuccPrelimit x) (hy : y < x) (n : ℕ) :

y + ↑n < x

theorem Order.IsPredPrelimit.lt_sub_natCast {α : Type u_1} {x y : α} [PartialOrder α] [AddCommGroupWithOne α] [PredSubOrder α] (hx : IsPredPrelimit x) (hy : x < y) (n : ℕ) :

x < y - ↑n

theorem Order.IsSuccLimit.add_natCast_lt {α : Type u_1} {x y : α} [PartialOrder α] [AddMonoidWithOne α] [SuccAddOrder α] (hx : IsSuccLimit x) (hy : y < x) (n : ℕ) :

y + ↑n < x

theorem Order.IsPredLimit.lt_sub_natCast {α : Type u_1} {x y : α} [PartialOrder α] [AddCommGroupWithOne α] [PredSubOrder α] (hx : IsPredLimit x) (hy : x < y) (n : ℕ) :

x < y - ↑n

theorem Order.IsSuccLimit.natCast_lt {α : Type u_1} {x : α} [PartialOrder α] [AddMonoidWithOne α] [SuccAddOrder α] [OrderBot α] [CanonicallyOrderedAdd α] (hx : IsSuccLimit x) (n : ℕ) :

↑n < x

theorem Order.not_isSuccLimit_natCast {α : Type u_1} [PartialOrder α] [AddMonoidWithOne α] [SuccAddOrder α] [OrderBot α] [CanonicallyOrderedAdd α] (n : ℕ) :

¬IsSuccLimit ↑n

@[simp]

theorem Order.succ_eq_zero {α : Type u_1} [PartialOrder α] [AddZeroClass α] [OrderBot α] [CanonicallyOrderedAdd α] [One α] [NoMaxOrder α] [SuccAddOrder α] {a : WithBot α} :

a.succ = 0 ↔ a = ⊥

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 a → a ∈ s → a + 1 ∈ s → f 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 a → a ∈ s → a + 1 ∈ s → f (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 a → a ∈ s → a + 1 ∈ s → f 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 a → a ∈ s → a + 1 ∈ s → f (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 a → f 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 a → f (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 a → f 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 a → f (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 a → a ∈ s → a - 1 ∈ s → f (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 a → a ∈ s → a - 1 ∈ s → f 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 a → a ∈ s → a - 1 ∈ s → f (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 a → a ∈ s → a - 1 ∈ s → f 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 a → f (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 a → f 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 a → f (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 a → f a < f (a - 1)) → StrictAnti f