def UpperBound {α : Type u_1} [Preorder α] (s : Set α) (a : α) : Prop

Equations

• UpperBound s a = ∀ (b : α), b ∈ s → b ≤ a

def LowerBound {α : Type u_1} [Preorder α] (s : Set α) (a : α) : Prop

Equations

• LowerBound s a = ∀ (b : α), b ∈ s → a ≤ b

def Set.BoundedAbove {α : Type u_1} [Preorder α] (s : Set α) : Prop

Equations

• s.BoundedAbove = ∃ (a : α), UpperBound s a

def Set.BoundedBelow {α : Type u_1} [Preorder α] (s : Set α) : Prop

Equations

• s.BoundedBelow = ∃ (a : α), LowerBound s a

def Set.Bounded {α : Type u_1} [Preorder α] (s : Set α) : Prop

Equations

• s.Bounded = (s.BoundedAbove ∧ s.BoundedBelow)

theorem upperBound_iff_greatest_of_mem {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : a ∈ s) : Greatest ⟨a, h⟩ ↔ UpperBound s a

theorem lowerBound_iff_least_of_mem {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : a ∈ s) : Least ⟨a, h⟩ ↔ LowerBound s a

theorem UpperBound.subset {α : Type u_1} [Preorder α] {s t : Set α} {a : α} (h : UpperBound s a) (h' : t ⊆ s) : UpperBound t a

theorem LowerBound.subset {α : Type u_1} [Preorder α] {s t : Set α} {a : α} (h : LowerBound s a) (h' : t ⊆ s) : LowerBound t a

theorem Set.BoundedAbove.subset {α : Type u_1} [Preorder α] {s t : Set α} (h : s.BoundedAbove) (h' : t ⊆ s) : t.BoundedAbove

theorem Set.BoundedBelow.subset {α : Type u_1} [Preorder α] {s t : Set α} (h : s.BoundedBelow) (h' : t ⊆ s) : t.BoundedBelow

theorem Set.Bounded.subset {α : Type u_1} [Preorder α] {s t : Set α} (h : s.Bounded) (h' : t ⊆ s) : t.Bounded

theorem UpperBound.upperBound_of_le {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : UpperBound s a) (h' : a ≤ b) : UpperBound s b

theorem LowerBound.lowerBound_of_le {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : LowerBound s a) (h' : b ≤ a) : LowerBound s b

theorem upperBound_iUnion_iff {α : Type u_1} [Preorder α] {a : α} {ι : Type u_3} {s : ι → Set α} : UpperBound (⋃ i : ι, s i) a ↔ ∀ (i : ι), UpperBound (s i) a

theorem UpperBound.upperBound_iInter {α : Type u_1} [Preorder α] {a : α} {ι : Type u_3} {s : ι → Set α} {i : ι} (h : UpperBound (s i) a) : UpperBound (⋂ i : ι, s i) a

theorem lowerbound_iUnion_iff {α : Type u_1} [Preorder α] {a : α} {ι : Type u_3} {s : ι → Set α} : LowerBound (⋃ i : ι, s i) a ↔ ∀ (i : ι), LowerBound (s i) a

theorem LowerBound.lowerBound_iInter {α : Type u_1} [Preorder α] {a : α} {ι : Type u_3} {s : ι → Set α} {i : ι} (h : LowerBound (s i) a) : LowerBound (⋂ i : ι, s i) a

@[simp]

theorem UpperBound.empty {α : Type u_1} [Preorder α] {a : α} : UpperBound ∅ a

@[simp]

theorem LowerBound.empty {α : Type u_1} [Preorder α] {a : α} : LowerBound ∅ a

@[simp]

theorem UpperBound.singleton {α : Type u_1} [Preorder α] {a b : α} : UpperBound {a} b ↔ a ≤ b

@[simp]

theorem LowerBound.singleton {α : Type u_1} [Preorder α] {a b : α} : LowerBound {a} b ↔ b ≤ a

theorem Monotone.upperBound_of_upperBound {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {a : α} {f : α → β} (h : Monotone f) (h' : UpperBound s a) : UpperBound (f '' s) (f a)

theorem Monotone.lowerBound_of_lowerBound {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {a : α} {f : α → β} (h : Monotone f) (h' : LowerBound s a) : LowerBound (f '' s) (f a)

@[simp]

theorem HasGreatest.upperBound {α : Type u_1} [Preorder α] [HasGreatest α] {s : Set α} : UpperBound s ⊤

@[simp]

theorem HasLeast.lowerBound {α : Type u_1} [Preorder α] [HasLeast α] {s : Set α} : LowerBound s ⊥