Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2021 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
! This file was ported from Lean 3 source module order.succ_pred.basic
! leanprover-community/mathlib commit 0111834459f5d7400215223ea95ae38a1265a907
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.CompleteLattice
import Mathlib.Order.Cover
import Mathlib.Order.Iterate
/-!
# Successor and predecessor
This file defines successor and predecessor orders. `succ a`, the successor of an element `a : α` is
the least element greater than `a`. `pred a` is the greatest element less than `a`. Typical examples
include `ℕ`, `ℤ`, `ℕ+`, `Fin n`, but also `ENat`, the lexicographic order of a successor/predecessor
order...
## Typeclasses
* `SuccOrder`: Order equipped with a sensible successor function.
* `PredOrder`: Order equipped with a sensible predecessor function.
* `IsSuccArchimedean`: `SuccOrder` where `succ` iterated to an element gives all the greater
ones.
* `IsPredArchimedean`: `PredOrder` where `pred` iterated to an element gives all the smaller
ones.
## Implementation notes
Maximal elements don't have a sensible successor. Thus the naïve typeclass
```lean
class NaiveSuccOrder (α : Type _) [Preorder α] :=
(succ : α → α)
(succ_le_iff : ∀ {a b}, succ a ≤ b ↔ a < b)
(lt_succ_iff : ∀ {a b}, a < succ b ↔ a ≤ b)
```
can't apply to an `OrderTop` because plugging in `a = b = ⊤` into either of `succ_le_iff` and
`lt_succ_iff` yields `⊤ < ⊤` (or more generally `m < m` for a maximal element `m`).
The solution taken here is to remove the implications `≤ → <` and instead require that `a < succ a`
for all non maximal elements (enforced by the combination of `le_succ` and the contrapositive of
`max_of_succ_le`).
The stricter condition of every element having a sensible successor can be obtained through the
combination of `SuccOrder α` and `NoMaxOrder α`.
## TODO
Is `GaloisConnection pred succ` always true? If not, we should introduce
```lean
class SuccPredOrder (α : Type _) [Preorder α] extends SuccOrder α, PredOrder α :=
(pred_succ_gc : GaloisConnection (pred : α → α) succ)
```
`Covby` should help here.
-/
open Function OrderDual Set
variable { α : Type _ : Type (?u.24483+1)}
/-- Order equipped with a sensible successor function. -/
@[ ext ]
class SuccOrder : {α : Type u_1} →
[inst : Preorder α (succ : α → α (∀ (a : α ), a ≤ succ a ) →
(∀ {a : α }, succ a ≤ a IsMax a ) →
(∀ {a b : α }, a < b succ a ≤ b ) → (∀ {a b : α }, a < succ b a ≤ b ) → SuccOrder α ( α : Type _ ) [ Preorder α ] where
/--Successor function-/
succ : α → α
/--Proof of basic ordering with respect to `succ`-/
le_succ : ∀ a , a ≤ succ a
/--Proof of interaction between `succ` and maximal element-/
max_of_succ_le { a } : succ a ≤ a → IsMax : {α : Type ?u.48} → [inst : LE α α → Prop a
/--Proof that `succ` satifies ordering invariants betweeen `LT` and `LE`-/
succ_le_of_lt { a b } : a < b → succ a ≤ b
/--Proof that `succ` satifies ordering invariants betweeen `LE` and `LT`-/
le_of_lt_succ { a b } : a < succ b → a ≤ b
#align succ_order SuccOrder
#align succ_order.ext_iff SuccOrder.ext_iff
#align succ_order.ext SuccOrder.ext
/-- Order equipped with a sensible predecessor function. -/
@[ ext ]
class PredOrder ( α : Type _ ) [ Preorder α ] where
/--Predecessor function-/
pred : α → α
/--Proof of basic ordering with respect to `pred`-/
pred_le : ∀ a , pred a ≤ a
/--Proof of interaction between `pred` and minimal element-/
min_of_le_pred { a } : a ≤ pred a → IsMin : {α : Type ?u.202} → [inst : LE α α → Prop a
/--Proof that `pred` satifies ordering invariants betweeen `LT` and `LE`-/
le_pred_of_lt { a b } : a < b → a ≤ pred b
/--Proof that `pred` satifies ordering invariants betweeen `LE` and `LT`-/
le_of_pred_lt { a b } : pred a < b → a ≤ b
#align pred_order PredOrder
#align pred_order.ext PredOrder.ext
#align pred_order.ext_iff PredOrder.ext_iff
instance [ Preorder α ] [ SuccOrder α ] :
PredOrder α ᵒᵈ where
pred := toDual : {α : Type ?u.360} → α ≃ α ᵒᵈ ∘ SuccOrder.succ ∘ ofDual : {α : Type ?u.465} → α ᵒᵈ ≃ α
pred_le := by
simp only [ comp : {α : Sort ?u.620} → {β : Sort ?u.619} → {δ : Sort ?u.618} → (β → δ (α → β α → δ , OrderDual.forall : ∀ {α : Type ?u.630} {p : α ᵒᵈ Prop (∀ (a : α ᵒᵈ p a ) ↔ ∀ (a : α ), p (↑toDual a ) , ofDual_toDual : ∀ {α : Type ?u.642} (a : α ), ↑ofDual (↑toDual a ) = a , toDual_le_toDual : ∀ {α : Type ?u.661} [inst : LE α a b : α }, ↑toDual a ≤ ↑toDual b ↔ b ≤ a ,
SuccOrder.le_succ , implies_true ]
min_of_le_pred h := by apply SuccOrder.max_of_succ_le h
le_pred_of_lt := by ∀ {a b : α ᵒᵈ a < b a ≤ (↑toDual ∘ SuccOrder.succ ∘ ↑ofDual b intro a b h ; ∀ {a b : α ᵒᵈ a < b a ≤ (↑toDual ∘ SuccOrder.succ ∘ ↑ofDual b exact SuccOrder.succ_le_of_lt h
le_of_pred_lt := SuccOrder.le_of_lt_succ
instance [ Preorder α ] [ PredOrder α ] :
SuccOrder α ᵒᵈ where
succ := toDual : {α : Type ?u.1299} → α ≃ α ᵒᵈ ∘ PredOrder.pred ∘ ofDual : {α : Type ?u.1405} → α ᵒᵈ ≃ α
le_succ := by
simp only [ comp : {α : Sort ?u.1567} → {β : Sort ?u.1566} → {δ : Sort ?u.1565} → (β → δ (α → β α → δ , OrderDual.forall : ∀ {α : Type ?u.1577} {p : α ᵒᵈ Prop (∀ (a : α ᵒᵈ p a ) ↔ ∀ (a : α ), p (↑toDual a ) , ofDual_toDual : ∀ {α : Type ?u.1589} (a : α ), ↑ofDual (↑toDual a ) = a , toDual_le_toDual : ∀ {α : Type ?u.1608} [inst : LE α a b : α }, ↑toDual a ≤ ↑toDual b ↔ b ≤ a ,
PredOrder.pred_le , implies_true ]
max_of_succ_le h := by apply PredOrder.min_of_le_pred h
succ_le_of_lt := by ∀ {a b : α ᵒᵈ a < b (↑toDual ∘ PredOrder.pred ∘ ↑ofDual a ≤ b intro a b h ; ∀ {a b : α ᵒᵈ a < b (↑toDual ∘ PredOrder.pred ∘ ↑ofDual a ≤ b exact PredOrder.le_pred_of_lt h
le_of_lt_succ := PredOrder.le_of_pred_lt
section Preorder
variable [ Preorder α ]
/-- A constructor for `SuccOrder α` usable when `α` has no maximal element. -/
def SuccOrder.ofSuccLeIffOfLeLtSucc : (succ : α → α (∀ {a b : α }, succ a ≤ b ↔ a < b ) → (∀ {a b : α }, a < succ b a ≤ b ) → SuccOrder α SuccOrder.ofSuccLeIffOfLeLtSucc ( succ : α → α ) ( hsucc_le_iff : ∀ {a b : α }, succ a ≤ b ↔ a < b hsucc_le_iff : ∀ { a b }, succ a ≤ b ↔ a < b )
( hle_of_lt_succ : ∀ {a b : α }, a < succ b a ≤ b hle_of_lt_succ : ∀ { a b }, a < succ b → a ≤ b ) : SuccOrder α :=
{ succ
le_succ := fun _ => ( hsucc_le_iff : ∀ {a b : α }, succ a ≤ b ↔ a < b hsucc_le_iff . 1 : ∀ {a b : Prop }, (a ↔ b a → b le_rfl ). le
max_of_succ_le := fun ha => ( lt_irrefl _ <| hsucc_le_iff : ∀ {a b : α }, succ a ≤ b ↔ a < b hsucc_le_iff . 1 : ∀ {a b : Prop }, (a ↔ b a → b ha ). elim
succ_le_of_lt := fun h => hsucc_le_iff : ∀ {a b : α }, succ a ≤ b ↔ a < b hsucc_le_iff . 2 : ∀ {a b : Prop }, (a ↔ b b → a h
le_of_lt_succ := fun h => hle_of_lt_succ : ∀ {a b : α }, a < succ b a ≤ b hle_of_lt_succ h }
#align succ_order.of_succ_le_iff_of_le_lt_succ SuccOrder.ofSuccLeIffOfLeLtSucc : {α : Type u_1} →
[inst : Preorder α (succ : α → α (∀ {a b : α }, succ a ≤ b ↔ a < b ) → (∀ {a b : α }, a < succ b a ≤ b ) → SuccOrder α
/-- A constructor for `PredOrder α` usable when `α` has no minimal element. -/
def PredOrder.ofLePredIffOfPredLePred : {α : Type u_1} →
[inst : Preorder α (pred : α → α (∀ {a b : α }, a ≤ pred b ↔ a < b ) → (∀ {a b : α }, pred a < b a ≤ b ) → PredOrder α PredOrder.ofLePredIffOfPredLePred ( pred : α → α ) ( hle_pred_iff : ∀ {a b : α }, a ≤ pred b ↔ a < b hle_pred_iff : ∀ { a b }, a ≤ pred b ↔ a < b )
( hle_of_pred_lt : ∀ {a b : α }, pred a < b a ≤ b hle_of_pred_lt : ∀ { a b }, pred a < b → a ≤ b ) : PredOrder α :=
{ pred
pred_le := fun _ => ( hle_pred_iff : ∀ {a b : α }, a ≤ pred b ↔ a < b hle_pred_iff . 1 : ∀ {a b : Prop }, (a ↔ b a → b le_rfl ). le
min_of_le_pred := fun ha => ( lt_irrefl _ <| hle_pred_iff : ∀ {a b : α }, a ≤ pred b ↔ a < b hle_pred_iff . 1 : ∀ {a b : Prop }, (a ↔ b a → b ha ). elim
le_pred_of_lt := fun h => hle_pred_iff : ∀ {a b : α }, a ≤ pred b ↔ a < b hle_pred_iff . 2 : ∀ {a b : Prop }, (a ↔ b b → a h
le_of_pred_lt := fun h => hle_of_pred_lt : ∀ {a b : α }, pred a < b a ≤ b hle_of_pred_lt h }
#align pred_order.of_le_pred_iff_of_pred_le_pred PredOrder.ofLePredIffOfPredLePred : {α : Type u_1} →
[inst : Preorder α (pred : α → α (∀ {a b : α }, a ≤ pred b ↔ a < b ) → (∀ {a b : α }, pred a < b a ≤ b ) → PredOrder α
end Preorder
section LinearOrder
variable [ LinearOrder : Type ?u.7313 → Type ?u.7313 α ]
/-- A constructor for `SuccOrder α` for `α` a linear order. -/
@[ simps ]
def SuccOrder.ofCore : (succ : α → α (∀ {a : α }, ¬ IsMax a ∀ (b : α ), a < b ↔ succ a ≤ b ) → (∀ (a : α ), IsMax a succ a = a ) → SuccOrder α SuccOrder.ofCore ( succ : α → α ) ( hn : ∀ {a : α }, ¬ IsMax a ∀ (b : α ), a < b ↔ succ a ≤ b hn : ∀ { a }, ¬ IsMax : {α : Type ?u.2775} → [inst : LE α α → Prop a → ∀ b , a < b ↔ succ a ≤ b )
( hm : ∀ (a : α ), IsMax a succ a = a hm : ∀ a , IsMax : {α : Type ?u.3006} → [inst : LE α α → Prop a → succ a = a ) : SuccOrder α :=
{ succ
succ_le_of_lt := fun { a b } =>
by_cases : ∀ {p q : Prop }, (p → q (¬ p q q ( fun h hab => ( hm : ∀ (a : α ), IsMax a succ a = a hm a h ). symm : ∀ {α : Sort ?u.3398} {a b : α }, a = b b = a symm ▸ hab . le ) fun h => ( hn : ∀ {a : α }, ¬ IsMax a ∀ (b : α ), a < b ↔ succ a ≤ b hn h b ). mp : ∀ {a b : Prop }, (a ↔ b a → b mp
le_succ := fun a =>
by_cases : ∀ {p q : Prop }, (p → q (¬ p q q ( fun h => ( hm : ∀ (a : α ), IsMax a succ a = a hm a h ). symm : ∀ {α : Sort ?u.3298} {a b : α }, a = b b = a symm . le ) fun h => le_of_lt : ∀ {α : Type ?u.3320} [inst : Preorder α a b : α }, a < b a ≤ b <| by simpa using ( hn : ∀ {a : α }, ¬ IsMax a ∀ (b : α ), a < b ↔ succ a ≤ b hn h a ). not : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b not
le_of_lt_succ := fun { a b } hab =>
by_cases : ∀ {p q : Prop }, (p → q (¬ p q q ( fun h => hm : ∀ (a : α ), IsMax a succ a = a hm b h ▸ hab . le ) fun h => by simpa [ hab ] using ( hn : ∀ {a : α }, ¬ IsMax a ∀ (b : α ), a < b ↔ succ a ≤ b hn h a ). not : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b not
max_of_succ_le := fun { a } => not_imp_not : ∀ {a b : Prop }, ¬ a ¬ b ↔ b → a . mp : ∀ {a b : Prop }, (a ↔ b a → b fun h => by simpa using ( hn : ∀ {a : α }, ¬ IsMax a ∀ (b : α ), a < b ↔ succ a ≤ b hn h a ). not : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b not }
#align succ_order.of_core SuccOrder.ofCore
#align succ_order.of_core_succ SuccOrder.ofCore_succ
/-- A constructor for `PredOrder α` for `α` a linear order. -/
@[ simps ]
def PredOrder.ofCore { α } [ LinearOrder : Type ?u.4594 → Type ?u.4594 α ] ( pred : α → α )
( hn : ∀ {a : α }, ¬ IsMin a ∀ (b : α ), b ≤ pred a ↔ b < a hn : ∀ { a }, ¬ IsMin : {α : Type ?u.4606} → [inst : LE α α → Prop a → ∀ b , b ≤ pred a ↔ b < a ) ( hm : ∀ (a : α ), IsMin a pred a = a hm : ∀ a , IsMin : {α : Type ?u.4911} → [inst : LE α α → Prop a → pred a = a ) :
PredOrder α :=
{ pred
le_pred_of_lt := fun { a b } =>
by_cases : ∀ {p q : Prop }, (p → q (¬ p q q ( fun h hab => ( hm : ∀ (a : α ), IsMin a pred a = a hm b h ). symm : ∀ {α : Sort ?u.5292} {a b : α }, a = b b = a symm ▸ hab . le ) fun h => ( hn : ∀ {a : α }, ¬ IsMin a ∀ (b : α ), b ≤ pred a ↔ b < a hn h a ). mpr : ∀ {a b : Prop }, (a ↔ b b → a mpr
pred_le := fun a =>
by_cases : ∀ {p q : Prop }, (p → q (¬ p q q ( fun h => ( hm : ∀ (a : α ), IsMin a pred a = a hm a h ). le ) fun h => le_of_lt : ∀ {α : Type ?u.5214} [inst : Preorder α a b : α }, a < b a ≤ b <| by simpa using ( hn : ∀ {a : α }, ¬ IsMin a ∀ (b : α ), b ≤ pred a ↔ b < a hn h a ). not : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b not
le_of_pred_lt := fun { a b } hab =>
by_cases : ∀ {p q : Prop }, (p → q (¬ p q q ( fun h => hm : ∀ (a : α ), IsMin a pred a = a hm a h ▸ hab . le ) fun h => by simpa [ hab ] using ( hn : ∀ {a : α }, ¬ IsMin a ∀ (b : α ), b ≤ pred a ↔ b < a hn h b ). not : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b not
min_of_le_pred := fun { a } => not_imp_not : ∀ {a b : Prop }, ¬ a ¬ b ↔ b → a . mp : ∀ {a b : Prop }, (a ↔ b a → b fun h => by simpa using ( hn : ∀ {a : α }, ¬ IsMin a ∀ (b : α ), b ≤ pred a ↔ b < a hn h a ). not : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b not }
#align pred_order.of_core PredOrder.ofCore
#align pred_order.of_core_pred PredOrder.ofCore_pred
/-- A constructor for `SuccOrder α` usable when `α` is a linear order with no maximal element. -/
def SuccOrder.ofSuccLeIff : (succ : α → α (∀ {a b : α }, succ a ≤ b ↔ a < b ) → SuccOrder α SuccOrder.ofSuccLeIff ( succ : α → α ) ( hsucc_le_iff : ∀ {a b : α }, succ a ≤ b ↔ a < b hsucc_le_iff : ∀ { a b }, succ a ≤ b ↔ a < b ) :
SuccOrder α :=
{ succ
le_succ := fun _ => ( hsucc_le_iff : ∀ {a b : α }, succ a ≤ b ↔ a < b hsucc_le_iff . 1 : ∀ {a b : Prop }, (a ↔ b a → b le_rfl ). le
max_of_succ_le := fun ha => ( lt_irrefl _ <| hsucc_le_iff : ∀ {a b : α }, succ a ≤ b ↔ a < b hsucc_le_iff . 1 : ∀ {a b : Prop }, (a ↔ b a → b ha ). elim
succ_le_of_lt := fun h => hsucc_le_iff : ∀ {a b : α }, succ a ≤ b ↔ a < b hsucc_le_iff . 2 : ∀ {a b : Prop }, (a ↔ b b → a h
le_of_lt_succ := fun { _ _ } h => le_of_not_lt (( not_congr : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b hsucc_le_iff : ∀ {a b : α }, succ a ≤ b ↔ a < b hsucc_le_iff ). 1 : ∀ {a b : Prop }, (a ↔ b a → b h . not_le ) }
#align succ_order.of_succ_le_iff SuccOrder.ofSuccLeIff
/-- A constructor for `PredOrder α` usable when `α` is a linear order with no minimal element. -/
def PredOrder.ofLePredIff : (pred : α → α (∀ {a b : α }, a ≤ pred b ↔ a < b ) → PredOrder α PredOrder.ofLePredIff ( pred : α → α ) ( hle_pred_iff : ∀ {a b : α }, a ≤ pred b ↔ a < b hle_pred_iff : ∀ { a b }, a ≤ pred b ↔ a < b ) :
PredOrder α :=
{ pred
pred_le := fun _ => ( hle_pred_iff : ∀ {a b : α }, a ≤ pred b ↔ a < b hle_pred_iff . 1 : ∀ {a b : Prop }, (a ↔ b a → b le_rfl ). le
min_of_le_pred := fun ha => ( lt_irrefl _ <| hle_pred_iff : ∀ {a b : α }, a ≤ pred b ↔ a < b hle_pred_iff . 1 : ∀ {a b : Prop }, (a ↔ b a → b ha ). elim
le_pred_of_lt := fun h => hle_pred_iff : ∀ {a b : α }, a ≤ pred b ↔ a < b hle_pred_iff . 2 : ∀ {a b : Prop }, (a ↔ b b → a h
le_of_pred_lt := fun { _ _ } h => le_of_not_lt (( not_congr : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b hle_pred_iff : ∀ {a b : α }, a ≤ pred b ↔ a < b hle_pred_iff ). 1 : ∀ {a b : Prop }, (a ↔ b a → b h . not_le ) }
#align pred_order.of_le_pred_iff PredOrder.ofLePredIff
end LinearOrder
/-! ### Successor order -/
namespace Order
section Preorder
variable [ Preorder α ] [ SuccOrder α ] { a b : α }
/-- The successor of an element. If `a` is not maximal, then `succ a` is the least element greater
than `a`. If `a` is maximal, then `succ a = a`. -/
def succ : α → α :=
SuccOrder.succ
#align order.succ Order.succ
theorem le_succ : ∀ a : α , a ≤ succ a :=
SuccOrder.le_succ
#align order.le_succ Order.le_succ
theorem max_of_succ_le { a : α } : succ a ≤ a → IsMax : {α : Type ?u.8219} → [inst : LE α α → Prop a :=
SuccOrder.max_of_succ_le
#align order.max_of_succ_le Order.max_of_succ_le
theorem succ_le_of_lt { a b : α } : a < b → succ a ≤ b :=
SuccOrder.succ_le_of_lt
#align order.succ_le_of_lt Order.succ_le_of_lt
theorem le_of_lt_succ { a b : α } : a < succ b → a ≤ b :=
SuccOrder.le_of_lt_succ
#align order.le_of_lt_succ Order.le_of_lt_succ
@[ simp ]
theorem succ_le_iff_isMax : succ a ≤ a ↔ IsMax : {α : Type ?u.8574} → [inst : LE α α → Prop a :=
⟨ max_of_succ_le , fun h => h <| le_succ _ ⟩
#align order.succ_le_iff_is_max Order.succ_le_iff_isMax
@[ simp ]
theorem lt_succ_iff_not_isMax : a < succ a ↔ ¬ IsMax : {α : Type ?u.8737} → [inst : LE α α → Prop a :=
⟨ not_isMax_of_lt , fun ha => ( le_succ a ). lt_of_not_le : ∀ {α : Type ?u.8799} [inst : Preorder α a b : α }, a ≤ b ¬ b ≤ a a < b lt_of_not_le fun h => ha <| max_of_succ_le h ⟩
#align order.lt_succ_iff_not_is_max Order.lt_succ_iff_not_isMax
alias lt_succ_iff_not_isMax ↔ _ lt_succ_of_not_isMax
#align order.lt_succ_of_not_is_max Order.lt_succ_of_not_isMax
theorem wcovby_succ ( a : α ) : a ⩿ succ a :=
⟨ le_succ a , fun _ hb => ( succ_le_of_lt hb ). not_lt ⟩
#align order.wcovby_succ Order.wcovby_succ
theorem covby_succ_of_not_isMax ( h : ¬ IsMax : {α : Type ?u.9046} → [inst : LE α α → Prop a ) : a ⋖ succ a :=
( wcovby_succ a ). covby_of_lt : ∀ {α : Type ?u.9126} [inst : Preorder α a b : α }, a ⩿ b a < b a ⋖ b covby_of_lt <| lt_succ_of_not_isMax h
#align order.covby_succ_of_not_is_max Order.covby_succ_of_not_isMax
theorem lt_succ_iff_of_not_isMax ( ha : ¬ IsMax : {α : Type ?u.9203} → [inst : LE α α → Prop a ) : b < succ a ↔ b ≤ a :=
⟨ le_of_lt_succ , fun h => h . trans_lt : ∀ {α : Type ?u.9300} [inst : Preorder α a b c : α }, a ≤ b b < c a < c <| lt_succ_of_not_isMax ha ⟩
#align order.lt_succ_iff_of_not_is_max Order.lt_succ_iff_of_not_isMax
theorem succ_le_iff_of_not_isMax ( ha : ¬ IsMax : {α : Type ?u.9371} → [inst : LE α α → Prop a ) : succ a ≤ b ↔ a < b :=
⟨( lt_succ_of_not_isMax ha ). trans_le : ∀ {α : Type ?u.9439} [inst : Preorder α a b c : α }, a < b b ≤ c a < c trans_le , succ_le_of_lt ⟩
#align order.succ_le_iff_of_not_is_max Order.succ_le_iff_of_not_isMax
theorem succ_lt_succ_iff_of_not_isMax ( ha : ¬ IsMax : {α : Type ?u.9518} → [inst : LE α α → Prop a ) ( hb : ¬ IsMax : {α : Type ?u.9533} → [inst : LE α α → Prop b ) : succ a < succ b ↔ a < b :=
by rw [ lt_succ_iff_of_not_isMax hb , succ_le_iff_of_not_isMax ha ]
#align order.succ_lt_succ_iff_of_not_is_max Order.succ_lt_succ_iff_of_not_isMax
theorem succ_le_succ_iff_of_not_isMax ( ha : ¬ IsMax : {α : Type ?u.9645} → [inst : LE α α → Prop a ) ( hb : ¬ IsMax : {α : Type ?u.9660} → [inst : LE α α → Prop b ) : succ a ≤ succ b ↔ a ≤ b :=
by rw [ succ_le_iff_of_not_isMax ha , lt_succ_iff_of_not_isMax hb ]
#align order.succ_le_succ_iff_of_not_is_max Order.succ_le_succ_iff_of_not_isMax
@[ simp , mono ]
theorem succ_le_succ ( h : a ≤ b ) : succ a ≤ succ b := by
by_cases hb : IsMax : {α : Type ?u.9803} → [inst : LE α α → Prop b
· by_cases hba : b ≤ a
· exact ( hb <| hba . trans : ∀ {α : Type ?u.9924} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c <| le_succ _ ). trans : ∀ {α : Type ?u.9968} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c trans ( le_succ _ )
· exact succ_le_of_lt (( h . lt_of_not_le : ∀ {α : Type ?u.10035} [inst : Preorder α a b : α }, a ≤ b ¬ b ≤ a a < b hba ). trans_le : ∀ {α : Type ?u.10048} [inst : Preorder α a b c : α }, a < b b ≤ c a < c trans_le <| le_succ b )
· rwa [ succ_le_iff_of_not_isMax fun ha => hb <| ha . mono h , lt_succ_iff_of_not_isMax hb ]
#align order.succ_le_succ Order.succ_le_succ
theorem succ_mono : Monotone ( succ : α → α ) := fun _ _ => succ_le_succ
#align order.succ_mono Order.succ_mono
theorem le_succ_iterate : ∀ (k : ℕ ) (x : α ), x ≤ (succ ^[ k ] ) x le_succ_iterate ( k : ℕ ) ( x : α ) : x ≤ ( succ ^[ k ]) x := by
conv_lhs => rw [ ( by simp only [ Function.iterate_id : ∀ {α : Type ?u.10550} (n : ℕ ), id ^[ n ] = id , id.def : ∀ {α : Sort ?u.10561} (a : α ), id a = a ] : x = (id^[k]) x) ]
exact Monotone.le_iterate_of_le succ_mono le_succ k x
#align order.le_succ_iterate Order.le_succ_iterate
theorem isMax_iterate_succ_of_eq_of_lt { n m : ℕ } ( h_eq : ( succ ^[ n ]) a = ( succ ^[ m ]) a )
( h_lt : n < m ) : IsMax : {α : Type ?u.10997} → [inst : LE α α → Prop (( succ ^[ n ]) a ) := by
refine' max_of_succ_le ( le_trans : ∀ {α : Type ?u.11103} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c _ h_eq . symm : ∀ {α : Sort ?u.11127} {a b : α }, a = b b = a . le : ∀ {α : Type ?u.11134} [inst : Preorder α a b : α }, a = b a ≤ b )
have : succ (( succ ^[ n ]) a ) = ( succ ^[ n + 1 ]) a := by rw [ Function.iterate_succ' , comp : {α : Sort ?u.11376} → {β : Sort ?u.11375} → {δ : Sort ?u.11374} → (β → δ (α → β α → δ ]
rw [ this ]
have h_le : n + 1 ≤ m := Nat.succ_le_of_lt h_lt
exact Monotone.monotone_iterate_of_le_map succ_mono ( le_succ a ) h_le
#align order.is_max_iterate_succ_of_eq_of_lt Order.isMax_iterate_succ_of_eq_of_lt
theorem isMax_iterate_succ_of_eq_of_ne { n m : ℕ } ( h_eq : ( succ ^[ n ]) a = ( succ ^[ m ]) a )
( h_ne : n ≠ m ) : IsMax : {α : Type ?u.11743} → [inst : LE α α → Prop (( succ ^[ n ]) a ) := by
cases' le_total n m with h h
· exact isMax_iterate_succ_of_eq_of_lt h_eq ( lt_of_le_of_ne h h_ne )
· rw [ h_eq ]
exact isMax_iterate_succ_of_eq_of_lt h_eq . symm : ∀ {α : Sort ?u.12123} {a b : α }, a = b b = a ( lt_of_le_of_ne h h_ne . symm : ∀ {α : Sort ?u.12156} {a b : α }, a ≠ b b ≠ a )
#align order.is_max_iterate_succ_of_eq_of_ne Order.isMax_iterate_succ_of_eq_of_ne
theorem Iio_succ_of_not_isMax ( ha : ¬ IsMax : {α : Type ?u.12201} → [inst : LE α α → Prop a ) : Iio ( succ a ) = Iic a :=
Set.ext : ∀ {α : Type ?u.12257} {a b : Set α (∀ (x : α ), x ∈ a ↔ x ∈ b ) → a = b fun _ => lt_succ_iff_of_not_isMax ha
#align order.Iio_succ_of_not_is_max Order.Iio_succ_of_not_isMax
theorem Ici_succ_of_not_isMax ( ha : ¬ IsMax : {α : Type ?u.12339} → [inst : LE α α → Prop a ) : Ici ( succ a ) = Ioi a :=
Set.ext : ∀ {α : Type ?u.12395} {a b : Set α (∀ (x : α ), x ∈ a ↔ x ∈ b ) → a = b fun _ => succ_le_iff_of_not_isMax ha
#align order.Ici_succ_of_not_is_max Order.Ici_succ_of_not_isMax
theorem Ico_succ_right_of_not_isMax ( hb : ¬ IsMax : {α : Type ?u.12477} → [inst : LE α α → Prop b ) : Ico a ( succ b ) = Icc a b := by
rw [ ← Ici_inter_Iio , Iio_succ_of_not_isMax hb , Ici_inter_Iic ]
#align order.Ico_succ_right_of_not_is_max Order.Ico_succ_right_of_not_isMax
theorem Ioo_succ_right_of_not_isMax ( hb : ¬ IsMax : {α : Type ?u.12669} → [inst : LE α α → Prop b ) : Ioo a ( succ b ) = Ioc a b := by
rw [ ← Ioi_inter_Iio , Iio_succ_of_not_isMax hb , Ioi_inter_Iic ]
#align order.Ioo_succ_right_of_not_is_max Order.Ioo_succ_right_of_not_isMax
theorem Icc_succ_left_of_not_isMax ( ha : ¬ IsMax : {α : Type ?u.12861} → [inst : LE α α → Prop a ) : Icc ( succ a ) b = Ioc a b := by
rw [ ← Ici_inter_Iic , Ici_succ_of_not_isMax ha , Ioi_inter_Iic ]
#align order.Icc_succ_left_of_not_is_max Order.Icc_succ_left_of_not_isMax
theorem Ico_succ_left_of_not_isMax ( ha : ¬ IsMax : {α : Type ?u.13053} → [inst : LE α α → Prop a ) : Ico ( succ a ) b = Ioo a b := by
rw [ ← Ici_inter_Iio , Ici_succ_of_not_isMax ha , Ioi_inter_Iio ]
#align order.Ico_succ_left_of_not_is_max Order.Ico_succ_left_of_not_isMax
section NoMaxOrder
variable [ NoMaxOrder : (α : Type ?u.14760) → [inst : LT α Prop α ]
theorem lt_succ ( a : α ) : a < succ a :=
lt_succ_of_not_isMax <| not_isMax a
#align order.lt_succ Order.lt_succ
@[ simp ]
theorem lt_succ_iff : a < succ b ↔ a ≤ b :=
lt_succ_iff_of_not_isMax <| not_isMax b
#align order.lt_succ_iff Order.lt_succ_iff
@[ simp ]
theorem succ_le_iff : succ a ≤ b ↔ a < b :=
succ_le_iff_of_not_isMax <| not_isMax a
#align order.succ_le_iff Order.succ_le_iff
theorem succ_le_succ_iff : succ a ≤ succ b ↔ a ≤ b := by simp
#align order.succ_le_succ_iff Order.succ_le_succ_iff
theorem succ_lt_succ_iff : succ a < succ b ↔ a < b := by simp
#align order.succ_lt_succ_iff Order.succ_lt_succ_iff
alias succ_le_succ_iff ↔ le_of_succ_le_succ _
#align order.le_of_succ_le_succ Order.le_of_succ_le_succ
alias succ_lt_succ_iff ↔ lt_of_succ_lt_succ succ_lt_succ
#align order.lt_of_succ_lt_succ Order.lt_of_succ_lt_succ
#align order.succ_lt_succ Order.succ_lt_succ
theorem succ_strictMono : StrictMono ( succ : α → α ) := fun _ _ => succ_lt_succ
#align order.succ_strict_mono Order.succ_strictMono
theorem covby_succ : ∀ (a : α ), a ⋖ succ a covby_succ ( a : α ) : a ⋖ succ a :=
covby_succ_of_not_isMax <| not_isMax a
#align order.covby_succ Order.covby_succ
@[ simp ]
theorem Iio_succ ( a : α ) : Iio ( succ a ) = Iic a :=