Documentation

Mathlib.Order.SuccPred.CompleteLinearOrder

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

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 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 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