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.

source

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 : α} (h : a ≤ b) : ∃ (n : ℕ), Order.succ^[n] a = b
If a ≤ b then one can get to a from b by iterating succ

Instances

source

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 : α} (h : a ≤ b) : ∃ (n : ℕ), Order.pred^[n] b = a
If a ≤ b then one can get to b from a by iterating pred

Instances

source

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

IsPredArchimedean αᵒᵈ

source

theorem LE.le.exists_succ_iterate {α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] {a b : α} (h : a ≤ b) :

∃ (n : ℕ), Order.succ^[n] a = b

source

theorem exists_succ_iterate_iff_le {α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] {a b : α} :

(∃ (n : ℕ), Order.succ^[n] a = b) ↔ a ≤ b

source

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.

source

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

source

theorem le_total_of_codirected {α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] {r v₁ v₂ : α} (h₁ : r ≤ v₁) (h₂ : r ≤ v₂) :

v₁ ≤ v₂ ∨ v₂ ≤ v₁

source

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

IsSuccArchimedean αᵒᵈ

source

theorem LE.le.exists_pred_iterate {α : Type u_1} [Preorder α] [PredOrder α] [IsPredArchimedean α] {a b : α} (h : a ≤ b) :

∃ (n : ℕ), Order.pred^[n] b = a

source

theorem exists_pred_iterate_iff_le {α : Type u_1} [Preorder α] [PredOrder α] [IsPredArchimedean α] {a b : α} :

(∃ (n : ℕ), Order.pred^[n] b = a) ↔ a ≤ b

source

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.

source

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

source

theorem le_total_of_directed {α : Type u_1} [Preorder α] [PredOrder α] [IsPredArchimedean α] {r v₁ v₂ : α} (h₁ : v₁ ≤ r) (h₂ : v₂ ≤ r) :

v₁ ≤ v₂ ∨ v₂ ≤ v₁

source

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₁

source

@[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] :

LinearOrder α

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

Equations

IsSuccArchimedean.linearOrder = LinearOrder.mk ⋯ inferInstance inferInstance inferInstance ⋯ ⋯ ⋯

Instances For

source

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₁

source

@[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] :

LinearOrder α

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

Equations

IsPredArchimedean.linearOrder = inferInstanceAs (LinearOrder αᵒᵈᵒᵈ)

Instances For

source

theorem succ_max {α : Type u_1} [LinearOrder α] [SuccOrder α] (a b : α) :

Order.succ (a ⊔ b) = Order.succ a ⊔ Order.succ b

source

theorem succ_min {α : Type u_1} [LinearOrder α] [SuccOrder α] (a b : α) :

Order.succ (a ⊓ b) = Order.succ a ⊓ Order.succ b

source

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

source

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

source

theorem pred_max {α : Type u_1} [LinearOrder α] [PredOrder α] (a b : α) :

Order.pred (a ⊔ b) = Order.pred a ⊔ Order.pred b

source

theorem pred_min {α : Type u_1} [LinearOrder α] [PredOrder α] (a b : α) :

Order.pred (a ⊓ b) = Order.pred a ⊓ Order.pred b

source

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

source

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

source

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)

source

@[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.

source

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)

source

@[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.

source

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)

source

@[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.

source

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)

source

@[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.

source

@[instance 100]

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

IsPredArchimedean α

source

@[instance 100]

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

IsSuccArchimedean α

source

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

source

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

source

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)

source

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

source

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

source

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.

source

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.

source

instance Set.OrdConnected.isPredArchimedean {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] (s : Set α) [s.OrdConnected] :

IsPredArchimedean ↑s

source

instance Set.OrdConnected.isSuccArchimedean {α : Type u_1} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] (s : Set α) [s.OrdConnected] :

IsSuccArchimedean ↑s

source

theorem monotoneOn_of_le_succ {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f a ≤ f (Order.succ a)) :

MonotoneOn f s

source

theorem antitoneOn_of_succ_le {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f (Order.succ a) ≤ f a) :

AntitoneOn f s

source

theorem strictMonoOn_of_lt_succ {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f a < f (Order.succ a)) :

StrictMonoOn f s

source

theorem strictAntiOn_of_succ_lt {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f (Order.succ a) < f a) :

StrictAntiOn f s

source

theorem monotone_of_le_succ {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {f : α → β} (hf : ∀ (a : α), ¬IsMax a → f a ≤ f (Order.succ a)) :

Monotone f

source

theorem antitone_of_succ_le {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {f : α → β} (hf : ∀ (a : α), ¬IsMax a → f (Order.succ a) ≤ f a) :

Antitone f

source

theorem strictMono_of_lt_succ {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {f : α → β} (hf : ∀ (a : α), ¬IsMax a → f a < f (Order.succ a)) :

StrictMono f

source

theorem strictAnti_of_succ_lt {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {f : α → β} (hf : ∀ (a : α), ¬IsMax a → f (Order.succ a) < f a) :

StrictAnti f

source

theorem monotoneOn_of_pred_le {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [PredOrder α] [IsPredArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMin a → a ∈ s → Order.pred a ∈ s → f (Order.pred a) ≤ f a) :

MonotoneOn f s

source

theorem antitoneOn_of_le_pred {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [PredOrder α] [IsPredArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMin a → a ∈ s → Order.pred a ∈ s → f a ≤ f (Order.pred a)) :

AntitoneOn f s

source

theorem strictMonoOn_of_pred_lt {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [PredOrder α] [IsPredArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMin a → a ∈ s → Order.pred a ∈ s → f (Order.pred a) < f a) :

StrictMonoOn f s

source

theorem strictAntiOn_of_lt_pred {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [PredOrder α] [IsPredArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMin a → a ∈ s → Order.pred a ∈ s → f a < f (Order.pred a)) :

StrictAntiOn f s

source

theorem monotone_of_pred_le {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [PredOrder α] [IsPredArchimedean α] {f : α → β} (hf : ∀ (a : α), ¬IsMin a → f (Order.pred a) ≤ f a) :

Monotone f

source

theorem antitone_of_le_pred {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [PredOrder α] [IsPredArchimedean α] {f : α → β} (hf : ∀ (a : α), ¬IsMin a → f a ≤ f (Order.pred a)) :

Antitone f

source

theorem strictMono_of_pred_lt {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [PredOrder α] [IsPredArchimedean α] {f : α → β} (hf : ∀ (a : α), ¬IsMin a → f (Order.pred a) < f a) :

StrictMono f

source

theorem strictAnti_of_lt_pred {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [PredOrder α] [IsPredArchimedean α] {f : α → β} (hf : ∀ (a : α), ¬IsMin a → f a < f (Order.pred a)) :

StrictAnti f

Documentation

Mathlib.Order.SuccPred.Archimedean

Archimedean successor and predecessor #