Strict bounds of a set

[UPSTREAM] The strict analogues of mathlib's upperBounds / lowerBounds: strictUpperBounds s is the set of points strictly above every element of s. mathlib has no strict-bounds primitive — strictness is usually routed through Set.Ioi / ssubset — so this file fills the gap as a sibling of upperBounds, modelled on it lemma-for-lemma. It backs the set-standard degree comparative ([Hoe83]'s S-comparative) and any "strictly exceeds a whole set" notion.

Main definitions

• strictUpperBounds / strictLowerBounds — the <-analogues of upperBounds / lowerBounds.

Main results

• mem_strictUpperBounds_iff_subset_Iio — x ∈ strictUpperBounds s ↔ s ⊆ Set.Iio x, the strict mirror of mem_upperBounds_iff_subset_Iic.
• strictUpperBounds_singleton — strictUpperBounds {a} = Set.Ioi a, the strict mirror of upperBounds_singleton.
• strictUpperBounds_subset_upperBounds — strict bounds are bounds.

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

The set of points strictly greater than every element of s. Strict analogue of upperBounds.

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. Strict analogue of lowerBounds.

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

theorem mem_strictUpperBounds_iff_subset_Iio {α : Type u_1} [Preorder α] {s : Set α} {x : α} : x ∈ strictUpperBounds s ↔ s ⊆ Set.Iio x

Strict mirror of mem_upperBounds_iff_subset_Iic.

theorem mem_strictLowerBounds_iff_subset_Ioi {α : Type u_1} [Preorder α] {s : Set α} {x : α} : x ∈ strictLowerBounds s ↔ s ⊆ Set.Ioi x

Strict mirror of mem_lowerBounds_iff_subset_Ici.

theorem strictUpperBounds_subset_upperBounds {α : Type u_1} [Preorder α] {s : Set α} : strictUpperBounds s ⊆ upperBounds s

theorem strictLowerBounds_subset_lowerBounds {α : Type u_1} [Preorder α] {s : Set α} : strictLowerBounds s ⊆ lowerBounds s

@[simp]

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

Strict mirror of upperBounds_singleton.

@[simp]

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

Strict mirror of lowerBounds_singleton.

@[simp]

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

@[simp]

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