Archimedean successor and predecessor

• 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.

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

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

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 α] : Prop

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

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

instance instIsPredArchimedeanOrderDual {α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] : IsPredArchimedean αᵒᵈ

Equations

• ⋯ = ⋯

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 ≤ n → P n → P (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

instance instIsSuccArchimedeanOrderDual {α : Type u_1} [Preorder α] [PredOrder α] [IsPredArchimedean α] : IsSuccArchimedean αᵒᵈ

Equations

• ⋯ = ⋯

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 : ∀ n ≤ m, P n → P (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 succ_max {α : Type u_1} [LinearOrder α] [SuccOrder α] (a : α) (b : α) : Order.succ (max a b) = max (Order.succ a) (Order.succ b)

theorem succ_min {α : Type u_1} [LinearOrder α] [SuccOrder α] (a : α) (b : α) : Order.succ (min a b) = min (Order.succ a) (Order.succ 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 : α) : Order.pred (max a b) = max (Order.pred a) (Order.pred b)

theorem pred_min {α : Type u_1} [LinearOrder α] [PredOrder α] (a : α) (b : α) : Order.pred (min a b) = min (Order.pred a) (Order.pred 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

theorem StrictMono.not_bddAbove_range_of_isSuccArchimedean {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] [Preorder β] {f : α → β} [NoMaxOrder α] [SuccOrder β] [IsSuccArchimedean β] (hf : StrictMono f) : ¬BddAbove (Set.range f)

@[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) : ¬BddAbove (Set.range f)

Alias of StrictMono.not_bddAbove_range_of_isSuccArchimedean.

theorem StrictMono.not_bddBelow_range_of_isPredArchimedean {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] [Preorder β] {f : α → β} [NoMinOrder α] [PredOrder β] [IsPredArchimedean β] (hf : StrictMono f) : ¬BddBelow (Set.range f)

@[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) : ¬BddBelow (Set.range f)

Alias of StrictMono.not_bddBelow_range_of_isPredArchimedean.

theorem StrictAnti.not_bddBelow_range_of_isSuccArchimedean {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] [Preorder β] {f : α → β} [NoMinOrder α] [SuccOrder β] [IsSuccArchimedean β] (hf : StrictAnti f) : ¬BddAbove (Set.range f)

@[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) : ¬BddAbove (Set.range f)

Alias of StrictAnti.not_bddBelow_range_of_isSuccArchimedean.

theorem StrictAnti.not_bddBelow_range_of_isPredArchimedean {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] [Preorder β] {f : α → β} [NoMaxOrder α] [PredOrder β] [IsPredArchimedean β] (hf : StrictAnti f) : ¬BddBelow (Set.range f)

@[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) : ¬BddBelow (Set.range f)

Alias of StrictAnti.not_bddBelow_range_of_isPredArchimedean.

@[instance 100]

instance WellFoundedLT.toIsPredArchimedean {α : Type u_1} [PartialOrder α] [h : WellFoundedLT α] [PredOrder α] : IsPredArchimedean α

Equations

• ⋯ = ⋯

@[instance 100]

instance WellFoundedGT.toIsSuccArchimedean {α : Type u_1} [PartialOrder α] [h : WellFoundedGT α] [SuccOrder α] : IsSuccArchimedean α

Equations

• ⋯ = ⋯

theorem Succ.rec_bot {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α] (p : α → Prop) (hbot : p ⊥) (hsucc : ∀ (a : α), p a → p (Order.succ a)) (a : α) : p a

theorem Pred.rec_top {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] [IsPredArchimedean α] (p : α → Prop) (htop : p ⊤) (hpred : ∀ (a : α), p a → p (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 IsSuccArchimedean.of_orderIso {X : Type u_3} {Y : Type u_4} [PartialOrder X] [PartialOrder Y] [SuccOrder X] [IsSuccArchimedean X] [SuccOrder Y] (f : X ≃o Y) : IsSuccArchimedean Y

IsSuccArchimedean transfers across equivalences between SuccOrders.

theorem IsPredArchimedean.of_orderIso {X : Type u_3} {Y : Type u_4} [PartialOrder X] [PartialOrder Y] [PredOrder X] [IsPredArchimedean X] [PredOrder Y] (f : X ≃o Y) : IsPredArchimedean Y

IsPredArchimedean transfers across equivalences between PredOrders.