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.
A typeclass for succ x = x + 1
.
- succ : α → α
- succ_eq_add_one (x : α) : SuccOrder.succ x = x + 1
Instances
A typeclass for pred x = x - 1
.
- pred : α → α
- pred_eq_sub_one (x : α) : PredOrder.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)
:
theorem
Order.add_one_le_iff
{α : Type u_1}
{x y : α}
[Preorder α]
[Add α]
[One α]
[SuccAddOrder α]
[NoMaxOrder α]
:
@[simp]
@[simp]
theorem
Order.covBy_add_one
{α : Type u_1}
[Preorder α]
[Add α]
[One α]
[SuccAddOrder α]
[NoMaxOrder α]
(x : α)
:
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)
:
theorem
Order.le_sub_one_iff
{α : Type u_1}
{x y : α}
[Preorder α]
[Sub α]
[One α]
[PredSubOrder α]
[NoMinOrder α]
:
@[simp]
@[simp]
theorem
Order.sub_one_covBy
{α : Type u_1}
[Preorder α]
[Sub α]
[One α]
[PredSubOrder α]
[NoMinOrder α]
(x : α)
:
@[simp]
theorem
Order.succ_iterate
{α : Type u_1}
[Preorder α]
[AddMonoidWithOne α]
[SuccAddOrder α]
(x : α)
(n : ℕ)
:
@[simp]
theorem
Order.pred_iterate
{α : Type u_1}
[Preorder α]
[AddCommGroupWithOne α]
[PredSubOrder α]
(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 α]
:
theorem
Order.covBy_iff_add_one_eq
{α : Type u_1}
{x y : α}
[PartialOrder α]
[Add α]
[One α]
[SuccAddOrder α]
[NoMaxOrder α]
:
theorem
Order.covBy_iff_sub_one_eq
{α : Type u_1}
{x y : α}
[PartialOrder α]
[Sub α]
[One α]
[PredSubOrder α]
[NoMinOrder α]
:
theorem
Order.IsSuccPrelimit.add_one_lt
{α : Type u_1}
{x y : α}
[PartialOrder α]
[Add α]
[One α]
[SuccAddOrder α]
(hx : Order.IsSuccPrelimit x)
(hy : y < x)
:
theorem
Order.IsPredPrelimit.lt_sub_one
{α : Type u_1}
{x y : α}
[PartialOrder α]
[Sub α]
[One α]
[PredSubOrder α]
(hx : Order.IsPredPrelimit x)
(hy : x < y)
:
theorem
Order.IsSuccLimit.add_one_lt
{α : Type u_1}
{x y : α}
[PartialOrder α]
[Add α]
[One α]
[SuccAddOrder α]
(hx : Order.IsSuccLimit x)
(hy : y < x)
:
theorem
Order.IsPredLimit.lt_sub_one
{α : Type u_1}
{x y : α}
[PartialOrder α]
[Sub α]
[One α]
[PredSubOrder α]
(hx : Order.IsPredLimit x)
(hy : x < y)
:
theorem
Order.IsSuccPrelimit.add_natCast_lt
{α : Type u_1}
{x y : α}
[PartialOrder α]
[AddMonoidWithOne α]
[SuccAddOrder α]
(hx : Order.IsSuccPrelimit x)
(hy : y < x)
(n : ℕ)
:
theorem
Order.IsPredPrelimit.lt_sub_natCast
{α : Type u_1}
{x y : α}
[PartialOrder α]
[AddCommGroupWithOne α]
[PredSubOrder α]
(hx : Order.IsPredPrelimit x)
(hy : 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 : ℕ)
:
theorem
Order.IsPredLimit.lt_sub_natCast
{α : Type u_1}
{x y : α}
[PartialOrder α]
[AddCommGroupWithOne α]
[PredSubOrder α]
(hx : Order.IsPredLimit x)
(hy : 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)
:
theorem
Order.lt_add_one_iff
{α : Type u_1}
{x y : α}
[LinearOrder α]
[Add α]
[One α]
[SuccAddOrder α]
[NoMaxOrder α]
:
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)
:
theorem
Order.sub_one_lt_iff
{α : Type u_1}
{x y : α}
[LinearOrder α]
[Sub α]
[One α]
[PredSubOrder α]
[NoMinOrder α]
:
theorem
Order.lt_one_iff_nonpos
{α : Type u_1}
{x : α}
[LinearOrder α]
[AddMonoidWithOne α]
[ZeroLEOneClass α]
[NeZero 1]
[SuccAddOrder α]
:
theorem
monotoneOn_of_le_add_one
{α : Type u_2}
{β : Type u_3}
[PartialOrder α]
[Preorder β]
[Add α]
[One α]
[SuccAddOrder α]
[IsSuccArchimedean α]
{s : Set α}
{f : α → β}
(hs : s.OrdConnected)
:
theorem
antitoneOn_of_add_one_le
{α : Type u_2}
{β : Type u_3}
[PartialOrder α]
[Preorder β]
[Add α]
[One α]
[SuccAddOrder α]
[IsSuccArchimedean α]
{s : Set α}
{f : α → β}
(hs : s.OrdConnected)
:
theorem
strictMonoOn_of_lt_add_one
{α : Type u_2}
{β : Type u_3}
[PartialOrder α]
[Preorder β]
[Add α]
[One α]
[SuccAddOrder α]
[IsSuccArchimedean α]
{s : Set α}
{f : α → β}
(hs : s.OrdConnected)
:
theorem
strictAntiOn_of_add_one_lt
{α : Type u_2}
{β : Type u_3}
[PartialOrder α]
[Preorder β]
[Add α]
[One α]
[SuccAddOrder α]
[IsSuccArchimedean α]
{s : Set α}
{f : α → β}
(hs : s.OrdConnected)
:
theorem
monotone_of_le_add_one
{α : Type u_2}
{β : Type u_3}
[PartialOrder α]
[Preorder β]
[Add α]
[One α]
[SuccAddOrder α]
[IsSuccArchimedean α]
{f : α → β}
:
theorem
antitone_of_add_one_le
{α : Type u_2}
{β : Type u_3}
[PartialOrder α]
[Preorder β]
[Add α]
[One α]
[SuccAddOrder α]
[IsSuccArchimedean α]
{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)
:
theorem
antitoneOn_of_le_sub_one
{α : Type u_2}
{β : Type u_3}
[PartialOrder α]
[Preorder β]
[Sub α]
[One α]
[PredSubOrder α]
[IsPredArchimedean α]
{s : Set α}
{f : α → β}
(hs : s.OrdConnected)
:
theorem
strictMonoOn_of_sub_one_lt
{α : Type u_2}
{β : Type u_3}
[PartialOrder α]
[Preorder β]
[Sub α]
[One α]
[PredSubOrder α]
[IsPredArchimedean α]
{s : Set α}
{f : α → β}
(hs : s.OrdConnected)
:
theorem
strictAntiOn_of_lt_sub_one
{α : Type u_2}
{β : Type u_3}
[PartialOrder α]
[Preorder β]
[Sub α]
[One α]
[PredSubOrder α]
[IsPredArchimedean α]
{s : Set α}
{f : α → β}
(hs : s.OrdConnected)
:
theorem
monotone_of_sub_one_le
{α : Type u_2}
{β : Type u_3}
[PartialOrder α]
[Preorder β]
[Sub α]
[One α]
[PredSubOrder α]
[IsPredArchimedean α]
{f : α → β}
:
theorem
antitone_of_le_sub_one
{α : Type u_2}
{β : Type u_3}
[PartialOrder α]
[Preorder β]
[Sub α]
[One α]
[PredSubOrder α]
[IsPredArchimedean α]
{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