Documentation

Mathlib.Order.SuccPred.Archimedean

Archimedean successor and predecessor #

class IsSuccArchimedean (α : Type u_3) [Preorder α] [SuccOrder α] :

A SuccOrder is succ-archimedean if one can go from any two comparable elements by iterating succ

  • exists_succ_iterate_of_le : ∀ {a b : α}, a b∃ (n : ), Order.succ^[n] a = b

    If a ≤ b then one can get to a from b by iterating succ

Instances
theorem IsSuccArchimedean.exists_succ_iterate_of_le {α : Type u_3} :
∀ {inst : Preorder α} {inst_1 : SuccOrder α} [self : IsSuccArchimedean α] {a b : α}, a b∃ (n : ), Order.succ^[n] a = b

If a ≤ b then one can get to a from b by iterating succ

class IsPredArchimedean (α : Type u_3) [Preorder α] [PredOrder α] :

A PredOrder is pred-archimedean if one can go from any two comparable elements by iterating pred

  • exists_pred_iterate_of_le : ∀ {a b : α}, a b∃ (n : ), Order.pred^[n] b = a

    If a ≤ b then one can get to b from a by iterating pred

Instances
theorem IsPredArchimedean.exists_pred_iterate_of_le {α : Type u_3} :
∀ {inst : Preorder α} {inst_1 : PredOrder α} [self : IsPredArchimedean α] {a b : α}, a b∃ (n : ), Order.pred^[n] b = a

If a ≤ b then one can get to b from a by iterating pred

theorem LE.le.exists_succ_iterate {α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] {a : α} {b : α} (h : a b) :
∃ (n : ), Order.succ^[n] a = b
theorem exists_succ_iterate_iff_le {α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] {a : α} {b : α} :
(∃ (n : ), Order.succ^[n] a = b) a b
theorem Succ.rec {α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] {P : αProp} {m : α} (h0 : P m) (h1 : ∀ (n : α), m nP nP (Order.succ n)) ⦃n : α (hmn : m n) :
P n

Induction principle on a type with a SuccOrder for all elements above a given element m.

theorem Succ.rec_iff {α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] {p : αProp} (hsucc : ∀ (a : α), p a p (Order.succ a)) {a : α} {b : α} (h : a b) :
p a p b
theorem le_total_of_codirected {α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] {r : α} {v₁ : α} {v₂ : α} (h₁ : r v₁) (h₂ : r v₂) :
v₁ v₂ v₂ v₁
theorem LE.le.exists_pred_iterate {α : Type u_1} [Preorder α] [PredOrder α] [IsPredArchimedean α] {a : α} {b : α} (h : a b) :
∃ (n : ), Order.pred^[n] b = a
theorem exists_pred_iterate_iff_le {α : Type u_1} [Preorder α] [PredOrder α] [IsPredArchimedean α] {a : α} {b : α} :
(∃ (n : ), Order.pred^[n] b = a) a b
theorem Pred.rec {α : Type u_1} [Preorder α] [PredOrder α] [IsPredArchimedean α] {P : αProp} {m : α} (h0 : P m) (h1 : nm, P nP (Order.pred n)) ⦃n : α (hmn : n m) :
P n

Induction principle on a type with a PredOrder for all elements below a given element m.

theorem Pred.rec_iff {α : Type u_1} [Preorder α] [PredOrder α] [IsPredArchimedean α] {p : αProp} (hsucc : ∀ (a : α), p a p (Order.pred a)) {a : α} {b : α} (h : a b) :
p a p b
theorem le_total_of_directed {α : Type u_1} [Preorder α] [PredOrder α] [IsPredArchimedean α] {r : α} {v₁ : α} {v₂ : α} (h₁ : v₁ r) (h₂ : v₂ r) :
v₁ v₂ v₂ v₁
theorem lt_or_le_of_codirected {α : Type u_1} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] {r : α} {v₁ : α} {v₂ : α} (h₁ : r v₁) (h₂ : r v₂) :
v₁ < v₂ v₂ v₁
@[reducible, inline]
abbrev IsSuccArchimedean.linearOrder {α : Type u_1} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] [DecidableEq α] [DecidableRel fun (x1 x2 : α) => x1 x2] [DecidableRel fun (x1 x2 : α) => x1 < x2] [IsDirected α fun (x1 x2 : α) => x1 x2] :

This isn't an instance due to a loop with LinearOrder.

Equations
  • IsSuccArchimedean.linearOrder = LinearOrder.mk inferInstance inferInstance inferInstance
theorem lt_or_le_of_directed {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] {r : α} {v₁ : α} {v₂ : α} (h₁ : v₁ r) (h₂ : v₂ r) :
v₁ < v₂ v₂ v₁
@[reducible, inline]
abbrev IsPredArchimedean.linearOrder {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [DecidableEq α] [DecidableRel fun (x1 x2 : α) => x1 x2] [DecidableRel fun (x1 x2 : α) => x1 < x2] [IsDirected α fun (x1 x2 : α) => x1 x2] :

This isn't an instance due to a loop with LinearOrder.

Equations
theorem succ_max {α : Type u_1} [LinearOrder α] [SuccOrder α] (a : α) (b : α) :
theorem succ_min {α : Type u_1} [LinearOrder α] [SuccOrder α] (a : α) (b : α) :
theorem exists_succ_iterate_or {α : Type u_1} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] {a : α} {b : α} :
(∃ (n : ), Order.succ^[n] a = b) ∃ (n : ), Order.succ^[n] b = a
theorem Succ.rec_linear {α : Type u_1} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] {p : αProp} (hsucc : ∀ (a : α), p a p (Order.succ a)) (a : α) (b : α) :
p a p b
theorem pred_max {α : Type u_1} [LinearOrder α] [PredOrder α] (a : α) (b : α) :
theorem pred_min {α : Type u_1} [LinearOrder α] [PredOrder α] (a : α) (b : α) :
theorem exists_pred_iterate_or {α : Type u_1} [LinearOrder α] [PredOrder α] [IsPredArchimedean α] {a : α} {b : α} :
(∃ (n : ), Order.pred^[n] b = a) ∃ (n : ), Order.pred^[n] a = b
theorem Pred.rec_linear {α : Type u_1} [LinearOrder α] [PredOrder α] [IsPredArchimedean α] {p : αProp} (hsucc : ∀ (a : α), p a p (Order.pred a)) (a : α) (b : α) :
p a p b
@[deprecated StrictMono.not_bddAbove_range_of_isSuccArchimedean]
theorem StrictMono.not_bddAbove_range {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] [Preorder β] {f : αβ} [NoMaxOrder α] [SuccOrder β] [IsSuccArchimedean β] (hf : StrictMono f) :

Alias of StrictMono.not_bddAbove_range_of_isSuccArchimedean.

@[deprecated StrictMono.not_bddBelow_range_of_isPredArchimedean]
theorem StrictMono.not_bddBelow_range {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] [Preorder β] {f : αβ} [NoMinOrder α] [PredOrder β] [IsPredArchimedean β] (hf : StrictMono f) :

Alias of StrictMono.not_bddBelow_range_of_isPredArchimedean.

@[deprecated StrictAnti.not_bddBelow_range_of_isSuccArchimedean]
theorem StrictAnti.not_bddAbove_range {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] [Preorder β] {f : αβ} [NoMinOrder α] [SuccOrder β] [IsSuccArchimedean β] (hf : StrictAnti f) :

Alias of StrictAnti.not_bddBelow_range_of_isSuccArchimedean.

@[deprecated StrictAnti.not_bddBelow_range_of_isPredArchimedean]
theorem StrictAnti.not_bddBelow_range {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] [Preorder β] {f : αβ} [NoMaxOrder α] [PredOrder β] [IsPredArchimedean β] (hf : StrictAnti f) :

Alias of StrictAnti.not_bddBelow_range_of_isPredArchimedean.

@[instance 100]
Equations
  • =
@[instance 100]
Equations
  • =
theorem Succ.rec_bot {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α] (p : αProp) (hbot : p ) (hsucc : ∀ (a : α), p ap (Order.succ a)) (a : α) :
p a
theorem Pred.rec_top {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] [IsPredArchimedean α] (p : αProp) (htop : p ) (hpred : ∀ (a : α), p ap (Order.pred a)) (a : α) :
p a
theorem SuccOrder.forall_ne_bot_iff {α : Type u_1} [Nontrivial α] [PartialOrder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α] (P : αProp) :
(∀ (i : α), i P i) ∀ (i : α), P (SuccOrder.succ i)
theorem BddAbove.exists_isGreatest_of_nonempty {X : Type u_3} [LinearOrder X] [SuccOrder X] [IsSuccArchimedean X] {S : Set X} (hS : BddAbove S) (hS' : S.Nonempty) :
∃ (x : X), IsGreatest S x
theorem BddBelow.exists_isLeast_of_nonempty {X : Type u_3} [LinearOrder X] [PredOrder X] [IsPredArchimedean X] {S : Set X} (hS : BddBelow S) (hS' : S.Nonempty) :
∃ (x : X), IsLeast S x

IsSuccArchimedean transfers across equivalences between SuccOrders.

IsPredArchimedean transfers across equivalences between PredOrders.

instance Set.OrdConnected.isPredArchimedean {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] (s : Set α) [s.OrdConnected] :
Equations
  • =
instance Set.OrdConnected.isSuccArchimedean {α : Type u_1} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] (s : Set α) [s.OrdConnected] :
Equations
  • =