theorem
Order.IsSuccLimit.sSup_Iio
{α : Type u_2}
[ConditionallyCompleteLattice α]
{x : α}
(h : IsSuccLimit x)
:
theorem
Order.IsPredLimit.sInf_Ioi
{α : Type u_2}
[ConditionallyCompleteLattice α]
{x : α}
(h : IsPredLimit x)
:
theorem
csSup_mem_of_not_isSuccLimit
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddAbove s)
(hlim : ¬Order.IsSuccLimit (sSup s))
:
theorem
csInf_mem_of_not_isPredLimit
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddBelow s)
(hcolim : ¬Order.IsPredLimit (sInf s))
:
theorem
exists_eq_ciSup_of_not_isSuccLimit
{ι : Sort u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[Nonempty ι]
{f : ι → α}
(hbdd : BddAbove (Set.range f))
(hf : ¬Order.IsSuccLimit (⨆ (i : ι), f i))
:
∃ (i : ι), f i = ⨆ (i : ι), f i
theorem
exists_eq_ciInf_of_not_isPredLimit
{ι : Sort u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[Nonempty ι]
{f : ι → α}
(hbdd : BddBelow (Set.range f))
(hf : ¬Order.IsPredLimit (⨅ (i : ι), f i))
:
∃ (i : ι), f i = ⨅ (i : ι), f i
@[deprecated csInf_mem_of_not_isPredLimit (since := "2026-04-24")]
theorem
csInf_mem_of_not_isPredPrelimit
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddBelow s)
(hlim : ¬Order.IsPredPrelimit (sInf s))
:
@[deprecated exists_eq_ciInf_of_not_isPredLimit (since := "2026-04-24")]
theorem
exists_eq_ciInf_of_not_isPredPrelimit
{ι : Sort u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[Nonempty ι]
{f : ι → α}
(hf : BddBelow (Set.range f))
(hf' : ¬Order.IsPredPrelimit (⨅ (i : ι), f i))
:
∃ (i : ι), f i = ⨅ (i : ι), f i
theorem
IsLUB.mem_of_nonempty_of_not_isSuccLimit
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
{x : α}
(hs : IsLUB s x)
(hne : s.Nonempty)
(hx : ¬Order.IsSuccLimit x)
:
theorem
IsGLB.mem_of_nonempty_of_not_isPredLimit
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
{x : α}
(hs : IsGLB s x)
(hne : s.Nonempty)
(hx : ¬Order.IsPredLimit x)
:
theorem
IsLUB.exists_of_nonempty_of_not_isSuccLimit
{ι : Sort u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[Nonempty ι]
{f : ι → α}
{x : α}
(hf : IsLUB (Set.range f) x)
(hx : ¬Order.IsSuccLimit x)
:
∃ (i : ι), f i = x
theorem
IsGLB.exists_of_nonempty_of_not_isPredLimit
{ι : Sort u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[Nonempty ι]
{f : ι → α}
{x : α}
(hf : IsGLB (Set.range f) x)
(hx : ¬Order.IsPredLimit x)
:
∃ (i : ι), f i = x
@[deprecated IsLUB.mem_of_nonempty_of_not_isSuccLimit (since := "2026-04-24")]
theorem
IsLUB.mem_of_nonempty_of_not_isSuccPrelimit
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
{x : α}
(hs : IsLUB s x)
(hne : s.Nonempty)
(hx : ¬Order.IsSuccPrelimit x)
:
@[deprecated IsGLB.mem_of_nonempty_of_not_isPredLimit (since := "2026-04-24")]
theorem
IsGLB.mem_of_nonempty_of_not_isPredPrelimit
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
{x : α}
(hs : IsGLB s x)
(hne : s.Nonempty)
(hx : ¬Order.IsPredPrelimit x)
:
@[deprecated IsLUB.exists_of_nonempty_of_not_isSuccLimit (since := "2026-04-24")]
theorem
IsLUB.exists_of_nonempty_of_not_isSuccPrelimit
{ι : Sort u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[Nonempty ι]
{f : ι → α}
{x : α}
(hf : IsLUB (Set.range f) x)
(hx : ¬Order.IsSuccPrelimit x)
:
∃ (i : ι), f i = x
@[deprecated IsGLB.exists_of_nonempty_of_not_isPredLimit (since := "2026-04-24")]
theorem
IsGLB.exists_of_nonempty_of_not_isPredPrelimit
{ι : Sort u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[Nonempty ι]
{f : ι → α}
{x : α}
(hf : IsGLB (Set.range f) x)
(hx : ¬Order.IsPredPrelimit x)
:
∃ (i : ι), f i = x
@[instance_reducible, deprecated SuccOrder.ofLinearWellFoundedLT (since := "2026-04-12")]
noncomputable def
ConditionallyCompleteLinearOrder.toSuccOrder
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[WellFoundedLT α]
:
Every conditionally complete linear order with well-founded < is a successor order, by setting
the successor of an element to be the infimum of all larger elements.
Instances For
theorem
csSup_mem_of_not_isSuccPrelimit
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{s : Set α}
(hlim : ¬Order.IsSuccPrelimit (sSup s))
:
See csSup_mem_of_not_isSuccLimit for the ConditionallyCompleteLinearOrder version.
@[deprecated csSup_mem_of_not_isSuccPrelimit (since := "2026-04-24")]
theorem
csSup_mem_of_not_isSuccPrelimit'
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{s : Set α}
(hlim : ¬Order.IsSuccPrelimit (sSup s))
:
Alias of csSup_mem_of_not_isSuccPrelimit.
See csSup_mem_of_not_isSuccLimit for the ConditionallyCompleteLinearOrder version.
theorem
exists_eq_ciSup_of_not_isSuccPrelimit
{ι : Sort u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{f : ι → α}
(hf' : ¬Order.IsSuccPrelimit (⨆ (i : ι), f i))
:
∃ (i : ι), f i = ⨆ (i : ι), f i
See exists_eq_ciSup_of_not_isSuccLimit for the ConditionallyCompleteLinearOrder version.
@[deprecated exists_eq_ciSup_of_not_isSuccPrelimit (since := "2026-04-24")]
theorem
exists_eq_ciSup_of_not_isSuccPrelimit'
{ι : Sort u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{f : ι → α}
(hf' : ¬Order.IsSuccPrelimit (⨆ (i : ι), f i))
:
∃ (i : ι), f i = ⨆ (i : ι), f i
Alias of exists_eq_ciSup_of_not_isSuccPrelimit.
See exists_eq_ciSup_of_not_isSuccLimit for the ConditionallyCompleteLinearOrder version.
theorem
Order.IsSuccPrelimit.sSup_Iio
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{x : α}
(h : IsSuccPrelimit x)
:
theorem
Order.IsSuccPrelimit.iSup_Iio
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{x : α}
(h : IsSuccPrelimit x)
:
theorem
Order.IsSuccLimit.iSup_Iio
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{x : α}
(h : IsSuccLimit x)
:
theorem
sSup_Iio_eq_self_iff_isSuccPrelimit
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{x : α}
:
theorem
iSup_Iio_eq_self_iff_isSuccPrelimit
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{x : α}
:
theorem
sSup_mem_of_not_isSuccPrelimit
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
(hlim : ¬Order.IsSuccPrelimit (sSup s))
:
theorem
sInf_mem_of_not_isPredPrelimit
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
(hcolim : ¬Order.IsPredPrelimit (sInf s))
:
theorem
exists_eq_iSup_of_not_isSuccPrelimit
{ι : Sort u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
(hf : ¬Order.IsSuccPrelimit (⨆ (i : ι), f i))
:
∃ (i : ι), f i = ⨆ (i : ι), f i
theorem
exists_eq_iInf_of_not_isPredPrelimit
{ι : Sort u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
(hf : ¬Order.IsPredPrelimit (⨅ (i : ι), f i))
:
∃ (i : ι), f i = ⨅ (i : ι), f i
theorem
sSup_lt_iff_of_not_isSuccPrelimit
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
{x : α}
(h : ¬Order.IsSuccPrelimit x)
:
Similar to sSup_lt_iff but with a weaker RHS, as it does not require a uniform bound.
theorem
lt_sInf_iff_of_not_isPredPrelimit
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
{x : α}
(h : ¬Order.IsPredPrelimit x)
:
Similar to lt_sInf_iff but with a weaker RHS, as it does not require a uniform bound.
theorem
iSup_lt_iff_of_not_isSuccPrelimit
{ι : Sort u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
{x : α}
(h : ¬Order.IsSuccPrelimit x)
:
Similar to iSup_lt_iff but with a weaker RHS, as it does not require a uniform bound.
theorem
lt_iInf_iff_of_not_isPredPrelimit
{ι : Sort u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
{x : α}
(h : ¬Order.IsPredPrelimit x)
:
Similar to lt_iInf_iff but with a weaker RHS, as it does not require a uniform bound.
theorem
le_sSup_iff_of_not_isSuccPrelimit
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
{x : α}
(h : ¬Order.IsSuccPrelimit x)
:
Similar to le_sSup_iff_forall_lt but with a stronger RHS, as it requires a uniform bound.
theorem
sInf_le_iff_of_not_isPredPrelimit
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
{x : α}
(h : ¬Order.IsPredPrelimit x)
:
Similar to sInf_le_iff_forall_lt but with a stronger RHS, as it requires a uniform bound.
theorem
le_iSup_iff_of_not_isSuccPrelimit
{ι : Sort u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
{x : α}
(h : ¬Order.IsSuccPrelimit x)
:
Similar to le_iSup_iff_forall_lt but with a stronger RHS, as it requires a uniform bound.
theorem
iInf_le_iff_of_not_isPredPrelimit
{ι : Sort u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
{x : α}
(h : ¬Order.IsPredPrelimit x)
:
Similar to iInf_le_iff_forall_lt but with a stronger RHS, as it requires a uniform bound.
theorem
Order.IsSuccPrelimit.sSup_lt_iff
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
{x : α}
(h : IsSuccPrelimit x)
:
Similar to sSup_lt_iff but with a stronger RHS, as it requires a strict inequality.
theorem
Order.IsPredPrelimit.lt_sInf_iff
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
{x : α}
(h : IsPredPrelimit x)
:
Similar to lt_sInf_iff but with a stronger RHS, as it requires a strict inequality.
theorem
Order.IsSuccPrelimit.iSup_lt_iff
{ι : Sort u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
{x : α}
(h : IsSuccPrelimit x)
:
Similar to iSup_lt_iff but with a stronger RHS, as it requires a strict inequality.
theorem
Order.IsPredPrelimit.lt_iInf_iff
{ι : Sort u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
{x : α}
(h : IsPredPrelimit x)
:
Similar to lt_iInf_iff but with a stronger RHS, as it requires a strict inequality.
theorem
Order.IsSuccPrelimit.le_sSup_iff
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
{x : α}
(h : IsSuccPrelimit x)
:
Similar to le_sSup_iff_forall_lt but with a weaker RHS, as it requires a non-strict
inequality.
theorem
Order.IsPredPrelimit.sInf_le_iff
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
{x : α}
(h : IsPredPrelimit x)
:
Similar to sInf_le_iff_forall_lt but with a weaker RHS, as it requires a non-strict
inequality.
theorem
Order.IsSuccPrelimit.le_iSup_iff
{ι : Sort u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
{x : α}
(h : IsSuccPrelimit x)
:
Similar to le_iSup_iff_forall_lt but with a weaker RHS, as it requires a non-strict
inequality.
theorem
Order.IsPredPrelimit.iInf_le_iff
{ι : Sort u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
{x : α}
(h : IsPredPrelimit x)
:
Similar to iInf_le_iff_forall_lt but with a weaker RHS, as it requires a non-strict
inequality.