Archimedean successor and predecessor #
IsSuccArchimedean:SuccOrderwheresucciterated to an element gives all the greater ones.IsPredArchimedean:PredOrderwhereprediterated to an element gives all the smaller ones.
A SuccOrder is succ-archimedean if one can go from any two comparable elements by iterating
succ
If
a ≤ bthen one can get toafrombby iteratingsucc
A PredOrder is pred-archimedean if one can go from any two comparable elements by iterating
pred
If
a ≤ bthen one can get tobfromaby iteratingpred
instance
instIsPredArchimedeanOrderDual
{α : Type u_1}
[Preorder α]
[SuccOrder α]
[IsSuccArchimedean α]
:
Equations
- ⋯ = ⋯
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 α]
:
Equations
- ⋯ = ⋯
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
lt_or_le_of_codirected
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
[IsSuccArchimedean α]
{r : α}
{v₁ : α}
{v₂ : α}
(h₁ : r ≤ v₁)
(h₂ : r ≤ 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)
:
@[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
- IsPredArchimedean.linearOrder = inferInstanceAs (LinearOrder αᵒᵈᵒᵈ)
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 : α}
:
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 : α}
:
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)
:
@[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.
theorem
StrictMono.not_bddBelow_range_of_isPredArchimedean
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Nonempty α]
[Preorder β]
{f : α → β}
[NoMinOrder α]
[PredOrder β]
[IsPredArchimedean β]
(hf : StrictMono 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)
:
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)
:
@[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.
theorem
StrictAnti.not_bddBelow_range_of_isPredArchimedean
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Nonempty α]
[Preorder β]
{f : α → β}
[NoMaxOrder α]
[PredOrder β]
[IsPredArchimedean β]
(hf : StrictAnti 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)
:
Alias of StrictAnti.not_bddBelow_range_of_isPredArchimedean.
@[instance 100]
instance
WellFoundedLT.toIsPredArchimedean
{α : Type u_1}
[PartialOrder α]
[h : WellFoundedLT α]
[PredOrder α]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
WellFoundedGT.toIsSuccArchimedean
{α : Type u_1}
[PartialOrder α]
[h : WellFoundedGT α]
[SuccOrder α]
:
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
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
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 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 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
- ⋯ = ⋯