HepLean Documentation

Mathlib.Order.SuccPred.CompleteLinearOrder

Relation between IsSuccPrelimit and iSup in (conditionally) complete linear orders. #

source
theorem csSup_mem_of_not_isSuccPrelimit {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) (hlim : ¬Order.IsSuccPrelimit (sSup s)) :
sSup s ∈ s
source
@[deprecated csSup_mem_of_not_isSuccPrelimit]
theorem csSup_mem_of_not_isSuccLimit {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) (hlim : ¬Order.IsSuccPrelimit (sSup s)) :
sSup s ∈ s

Alias of csSup_mem_of_not_isSuccPrelimit.

source
theorem csInf_mem_of_not_isPredPrelimit {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) (hlim : ¬Order.IsPredPrelimit (sInf s)) :
sInf s ∈ s
source
@[deprecated csInf_mem_of_not_isPredPrelimit]
theorem csInf_mem_of_not_isPredLimit {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) (hlim : ¬Order.IsPredPrelimit (sInf s)) :
sInf s ∈ s

Alias of csInf_mem_of_not_isPredPrelimit.

source
theorem exists_eq_ciSup_of_not_isSuccPrelimit {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} (hf : BddAbove (Set.range f)) (hf' : ¬Order.IsSuccPrelimit (⨆ (i : ι), f i)) :
∃ (i : ι), f i = ⨆ (i : ι), f i
source
@[deprecated exists_eq_ciSup_of_not_isSuccPrelimit]
theorem exists_eq_ciSup_of_not_isSuccLimit {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} (hf : BddAbove (Set.range f)) (hf' : ¬Order.IsSuccPrelimit (⨆ (i : ι), f i)) :
∃ (i : ι), f i = ⨆ (i : ι), f i

Alias of exists_eq_ciSup_of_not_isSuccPrelimit.

source
theorem exists_eq_ciInf_of_not_isPredPrelimit {ι : Type 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
source
@[deprecated exists_eq_ciInf_of_not_isPredPrelimit]
theorem exists_eq_ciInf_of_not_isPredLimit {ι : Type 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

Alias of exists_eq_ciInf_of_not_isPredPrelimit.

source
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) :
x ∈ s
source
@[deprecated IsLUB.mem_of_nonempty_of_not_isSuccPrelimit]
theorem IsLUB.mem_of_nonempty_of_not_isSuccLimit {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} {x : α} (hs : IsLUB s x) (hne : s.Nonempty) (hx : ¬Order.IsSuccPrelimit x) :
x ∈ s

Alias of IsLUB.mem_of_nonempty_of_not_isSuccPrelimit.

source
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) :
x ∈ s
source
@[deprecated IsGLB.mem_of_nonempty_of_not_isPredPrelimit]
theorem IsGLB.mem_of_nonempty_of_not_isPredLimit {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} {x : α} (hs : IsGLB s x) (hne : s.Nonempty) (hx : ¬Order.IsPredPrelimit x) :
x ∈ s

Alias of IsGLB.mem_of_nonempty_of_not_isPredPrelimit.

source
theorem IsLUB.exists_of_nonempty_of_not_isSuccPrelimit {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} {x : α} (hf : IsLUB (Set.range f) x) (hx : ¬Order.IsSuccPrelimit x) :
∃ (i : ι), f i = x
source
@[deprecated IsLUB.exists_of_nonempty_of_not_isSuccPrelimit]
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.IsSuccPrelimit x) :
∃ (i : ι), f i = x

Alias of IsLUB.exists_of_nonempty_of_not_isSuccPrelimit.

source
theorem IsGLB.exists_of_nonempty_of_not_isPredPrelimit {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} {x : α} (hf : IsGLB (Set.range f) x) (hx : ¬Order.IsPredPrelimit x) :
∃ (i : ι), f i = x
source
@[deprecated IsGLB.exists_of_nonempty_of_not_isPredPrelimit]
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.IsPredPrelimit x) :
∃ (i : ι), f i = x

Alias of IsGLB.exists_of_nonempty_of_not_isPredPrelimit.

source
noncomputable def ConditionallyCompleteLinearOrder.toSuccOrder {α : Type u_2} [ConditionallyCompleteLinearOrder α] [WellFoundedLT α] :
SuccOrder α

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.

Equations
  • ConditionallyCompleteLinearOrder.toSuccOrder = { succ := fun (a : α) => if IsMax a then a else sInf {b : α | a < b}, le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
Instances For
    source
    theorem csSup_mem_of_not_isSuccPrelimit' {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {s : Set α} (hbdd : BddAbove s) (hlim : ¬Order.IsSuccPrelimit (sSup s)) :
    sSup s ∈ s

    See csSup_mem_of_not_isSuccPrelimit for the ConditionallyCompleteLinearOrder version.

    source
    @[deprecated csSup_mem_of_not_isSuccPrelimit']
    theorem csSup_mem_of_not_isSuccLimit' {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {s : Set α} (hbdd : BddAbove s) (hlim : ¬Order.IsSuccPrelimit (sSup s)) :
    sSup s ∈ s

    Alias of csSup_mem_of_not_isSuccPrelimit'.

    See csSup_mem_of_not_isSuccPrelimit for the ConditionallyCompleteLinearOrder version.

    source
    theorem exists_eq_ciSup_of_not_isSuccPrelimit' {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {f : ι → α} (hf : BddAbove (Set.range f)) (hf' : ¬Order.IsSuccPrelimit (⨆ (i : ι), f i)) :
    ∃ (i : ι), f i = ⨆ (i : ι), f i

    See exists_eq_ciSup_of_not_isSuccPrelimit for the ConditionallyCompleteLinearOrder version.

    source
    @[deprecated exists_eq_ciSup_of_not_isSuccPrelimit']
    theorem exists_eq_ciSup_of_not_isSuccLimit' {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {f : ι → α} (hf : BddAbove (Set.range 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_isSuccPrelimit for the ConditionallyCompleteLinearOrder version.

    source
    theorem IsLUB.mem_of_not_isSuccPrelimit {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {x : α} (hs : IsLUB s x) (hx : ¬Order.IsSuccPrelimit x) :
    x ∈ s
    source
    @[deprecated IsLUB.mem_of_not_isSuccPrelimit]
    theorem IsLUB.mem_of_not_isSuccLimit {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {x : α} (hs : IsLUB s x) (hx : ¬Order.IsSuccPrelimit x) :
    x ∈ s

    Alias of IsLUB.mem_of_not_isSuccPrelimit.

    source
    theorem IsLUB.exists_of_not_isSuccPrelimit {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {f : ι → α} {x : α} (hf : IsLUB (Set.range f) x) (hx : ¬Order.IsSuccPrelimit x) :
    ∃ (i : ι), f i = x
    source
    @[deprecated IsLUB.exists_of_not_isSuccPrelimit]
    theorem IsLUB.exists_of_not_isSuccLimit {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {f : ι → α} {x : α} (hf : IsLUB (Set.range f) x) (hx : ¬Order.IsSuccPrelimit x) :
    ∃ (i : ι), f i = x

    Alias of IsLUB.exists_of_not_isSuccPrelimit.

    source
    theorem sSup_mem_of_not_isSuccPrelimit {α : Type u_2} [CompleteLinearOrder α] {s : Set α} (hlim : ¬Order.IsSuccPrelimit (sSup s)) :
    sSup s ∈ s
    source
    @[deprecated sSup_mem_of_not_isSuccPrelimit]
    theorem sSup_mem_of_not_isSuccLimit {α : Type u_2} [CompleteLinearOrder α] {s : Set α} (hlim : ¬Order.IsSuccPrelimit (sSup s)) :
    sSup s ∈ s

    Alias of sSup_mem_of_not_isSuccPrelimit.

    source
    theorem sInf_mem_of_not_isPredPrelimit {α : Type u_2} [CompleteLinearOrder α] {s : Set α} (hlim : ¬Order.IsPredPrelimit (sInf s)) :
    sInf s ∈ s
    source
    @[deprecated sInf_mem_of_not_isPredPrelimit]
    theorem sInf_mem_of_not_isPredLimit {α : Type u_2} [CompleteLinearOrder α] {s : Set α} (hlim : ¬Order.IsPredPrelimit (sInf s)) :
    sInf s ∈ s

    Alias of sInf_mem_of_not_isPredPrelimit.

    source
    theorem exists_eq_iSup_of_not_isSuccPrelimit {ι : Type u_1} {α : Type u_2} [CompleteLinearOrder α] {f : ι → α} (hf : ¬Order.IsSuccPrelimit (⨆ (i : ι), f i)) :
    ∃ (i : ι), f i = ⨆ (i : ι), f i
    source
    @[deprecated exists_eq_iSup_of_not_isSuccPrelimit]
    theorem exists_eq_iSup_of_not_isSuccLimit {ι : Type u_1} {α : Type u_2} [CompleteLinearOrder α] {f : ι → α} (hf : ¬Order.IsSuccPrelimit (⨆ (i : ι), f i)) :
    ∃ (i : ι), f i = ⨆ (i : ι), f i

    Alias of exists_eq_iSup_of_not_isSuccPrelimit.

    source
    theorem exists_eq_iInf_of_not_isPredPrelimit {ι : Type u_1} {α : Type u_2} [CompleteLinearOrder α] {f : ι → α} (hf : ¬Order.IsPredPrelimit (⨅ (i : ι), f i)) :
    ∃ (i : ι), f i = ⨅ (i : ι), f i
    source
    @[deprecated exists_eq_iInf_of_not_isPredPrelimit]
    theorem exists_eq_iInf_of_not_isPredLimit {ι : Type u_1} {α : Type u_2} [CompleteLinearOrder α] {f : ι → α} (hf : ¬Order.IsPredPrelimit (⨅ (i : ι), f i)) :
    ∃ (i : ι), f i = ⨅ (i : ι), f i

    Alias of exists_eq_iInf_of_not_isPredPrelimit.

    source
    theorem IsGLB.mem_of_not_isPredPrelimit {α : Type u_2} [CompleteLinearOrder α] {s : Set α} {x : α} (hs : IsGLB s x) (hx : ¬Order.IsPredPrelimit x) :
    x ∈ s
    source
    @[deprecated IsGLB.mem_of_not_isPredPrelimit]
    theorem IsGLB.mem_of_not_isPredLimit {α : Type u_2} [CompleteLinearOrder α] {s : Set α} {x : α} (hs : IsGLB s x) (hx : ¬Order.IsPredPrelimit x) :
    x ∈ s

    Alias of IsGLB.mem_of_not_isPredPrelimit.

    source
    theorem IsGLB.exists_of_not_isPredPrelimit {ι : Type u_1} {α : Type u_2} [CompleteLinearOrder α] {f : ι → α} {x : α} (hf : IsGLB (Set.range f) x) (hx : ¬Order.IsPredPrelimit x) :
    ∃ (i : ι), f i = x
    source
    @[deprecated IsGLB.exists_of_not_isPredPrelimit]
    theorem IsGLB.exists_of_not_isPredLimit {ι : Type u_1} {α : Type u_2} [CompleteLinearOrder α] {f : ι → α} {x : α} (hf : IsGLB (Set.range f) x) (hx : ¬Order.IsPredPrelimit x) :
    ∃ (i : ι), f i = x

    Alias of IsGLB.exists_of_not_isPredPrelimit.