theorem
csSup_mem_of_not_isSuccLimit
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
(hne : Set.Nonempty s)
(hbdd : BddAbove s)
(hlim : ¬Order.IsSuccLimit (sSup s))
:
theorem
csInf_mem_of_not_isPredLimit
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
(hne : Set.Nonempty s)
(hbdd : BddBelow s)
(hlim : ¬Order.IsPredLimit (sInf s))
:
theorem
exists_eq_ciSup_of_not_isSuccLimit
{ι : Type u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[Nonempty ι]
{f : ι → α}
(hf : BddAbove (Set.range f))
(hf' : ¬Order.IsSuccLimit (⨆ (i : ι), f i))
:
∃ (i : ι), f i = ⨆ (i : ι), f i
theorem
exists_eq_ciInf_of_not_isPredLimit
{ι : Type u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[Nonempty ι]
{f : ι → α}
(hf : BddBelow (Set.range f))
(hf' : ¬Order.IsPredLimit (⨅ (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 : Set.Nonempty s)
(hx : ¬Order.IsSuccLimit x)
:
x ∈ s
theorem
IsGLB.mem_of_nonempty_of_not_isPredLimit
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
{x : α}
(hs : IsGLB s x)
(hne : Set.Nonempty s)
(hx : ¬Order.IsPredLimit x)
:
x ∈ s
theorem
IsLUB.exists_of_nonempty_of_not_isSuccLimit
{ι : Type 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
{ι : Type u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[Nonempty ι]
{f : ι → α}
{x : α}
(hf : IsGLB (Set.range f) x)
(hx : ¬Order.IsPredLimit x)
:
∃ (i : ι), f i = x
theorem
csSup_mem_of_not_isSuccLimit'
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{s : Set α}
(hbdd : BddAbove s)
(hlim : ¬Order.IsSuccLimit (sSup s))
:
See csSup_mem_of_not_isSuccLimit for the ConditionallyCompleteLinearOrder version.
theorem
exists_eq_ciSup_of_not_isSuccLimit'
{ι : Type u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{f : ι → α}
(hf : BddAbove (Set.range f))
(hf' : ¬Order.IsSuccLimit (⨆ (i : ι), f i))
:
∃ (i : ι), f i = ⨆ (i : ι), f i
See exists_eq_ciSup_of_not_isSuccLimit for the
ConditionallyCompleteLinearOrder version.
theorem
IsLUB.mem_of_not_isSuccLimit
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{s : Set α}
{x : α}
(hs : IsLUB s x)
(hx : ¬Order.IsSuccLimit x)
:
x ∈ s
theorem
IsLUB.exists_of_not_isSuccLimit
{ι : Type u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{f : ι → α}
{x : α}
(hf : IsLUB (Set.range f) x)
(hx : ¬Order.IsSuccLimit x)
:
∃ (i : ι), f i = x
theorem
sSup_mem_of_not_isSuccLimit
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
(hlim : ¬Order.IsSuccLimit (sSup s))
:
theorem
sInf_mem_of_not_isPredLimit
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
(hlim : ¬Order.IsPredLimit (sInf s))
:
theorem
exists_eq_iSup_of_not_isSuccLimit
{ι : Type u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
(hf : ¬Order.IsSuccLimit (⨆ (i : ι), f i))
:
∃ (i : ι), f i = ⨆ (i : ι), f i
theorem
exists_eq_iInf_of_not_isPredLimit
{ι : Type u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
(hf : ¬Order.IsPredLimit (⨅ (i : ι), f i))
:
∃ (i : ι), f i = ⨅ (i : ι), f i
theorem
IsGLB.mem_of_not_isPredLimit
{α : Type u_2}
[CompleteLinearOrder α]
{s : Set α}
{x : α}
(hs : IsGLB s x)
(hx : ¬Order.IsPredLimit x)
:
x ∈ s
theorem
IsGLB.exists_of_not_isPredLimit
{ι : Type u_1}
{α : Type u_2}
[CompleteLinearOrder α]
{f : ι → α}
{x : α}
(hf : IsGLB (Set.range f) x)
(hx : ¬Order.IsPredLimit x)
:
∃ (i : ι), f i = x