Strict bounds of a set

[UPSTREAM] The strict analogues of mathlib's upperBounds and lowerBounds: strictUpperBounds s is the set of points strictly above every element of s. Mathlib has no strict-bounds primitive, routing strictness through Set.Ioi or ssubset instead.

def strictUpperBounds {α : Type u_1} [Preorder α] (s : Set α) : Set α

The set of points strictly greater than every element of s.

Equations

• strictUpperBounds s = {x : α | ∀ ⦃a : α⦄, a ∈ s → a < x}

def strictLowerBounds {α : Type u_1} [Preorder α] (s : Set α) : Set α

The set of points strictly less than every element of s.

Equations

• strictLowerBounds s = {x : α | ∀ ⦃a : α⦄, a ∈ s → x < a}

theorem mem_strictUpperBounds {α : Type u_1} [Preorder α] {s : Set α} {x : α} : x ∈ strictUpperBounds s ↔ ∀ ⦃a : α⦄, a ∈ s → a < x

theorem mem_strictLowerBounds {α : Type u_1} [Preorder α] {s : Set α} {x : α} : x ∈ strictLowerBounds s ↔ ∀ ⦃a : α⦄, a ∈ s → x < a

@[simp]

theorem strictUpperBounds_singleton {α : Type u_1} [Preorder α] {a : α} : strictUpperBounds {a} = Set.Ioi a

@[simp]

theorem strictLowerBounds_singleton {α : Type u_1} [Preorder α] {a : α} : strictLowerBounds {a} = Set.Iio a

@[simp]

theorem strictUpperBounds_empty {α : Type u_1} [Preorder α] : strictUpperBounds ∅ = Set.univ

@[simp]

theorem strictLowerBounds_empty {α : Type u_1} [Preorder α] : strictLowerBounds ∅ = Set.univ