Upper / lower bounds

In this file we define:

• upperBounds, lowerBounds : the set of upper bounds (resp., lower bounds) of a set;
• BddAbove s, BddBelow s : the set s is bounded above (resp., below), i.e., the set of upper (resp., lower) bounds of s is nonempty;
• IsLeast s a, IsGreatest s a : a is a least (resp., greatest) element of s; for a partial order, it is unique if exists;
• IsLUB s a, IsGLB s a : a is a least upper bound (resp., a greatest lower bound) of s; for a partial order, it is unique if exists. We also prove various lemmas about monotonicity, behaviour under ∪, ∩, insert, and provide formulas for ∅, univ, and intervals.

Definitions

def upperBounds {α : Type u} [Preorder α] (s : Set α) : Set α

The set of upper bounds of a set.

Equations

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

def lowerBounds {α : Type u} [Preorder α] (s : Set α) : Set α

The set of lower bounds of a set.

Equations

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

def BddAbove {α : Type u} [Preorder α] (s : Set α) : Prop

A set is bounded above if there exists an upper bound.

Equations

• BddAbove s = Set.Nonempty (upperBounds s)

def BddBelow {α : Type u} [Preorder α] (s : Set α) : Prop

A set is bounded below if there exists a lower bound.

Equations

• BddBelow s = Set.Nonempty (lowerBounds s)

def IsLeast {α : Type u} [Preorder α] (s : Set α) (a : α) : Prop

a is a least element of a set s; for a partial order, it is unique if exists.

Equations

• IsLeast s a = (a ∈ s ∧ a ∈ lowerBounds s)

def IsGreatest {α : Type u} [Preorder α] (s : Set α) (a : α) : Prop

a is a greatest element of a set s; for a partial order, it is unique if exists

Equations

• IsGreatest s a = (a ∈ s ∧ a ∈ upperBounds s)

def IsLUB {α : Type u} [Preorder α] (s : Set α) : α → Prop

a is a least upper bound of a set s; for a partial order, it is unique if exists.

Equations

• IsLUB s = IsLeast (upperBounds s)

def IsGLB {α : Type u} [Preorder α] (s : Set α) : α → Prop

a is a greatest lower bound of a set s; for a partial order, it is unique if exists.

Equations

• IsGLB s = IsGreatest (lowerBounds s)

theorem mem_upperBounds {α : Type u} [Preorder α] {s : Set α} {a : α} : a ∈ upperBounds s ↔ ∀ (x : α), x ∈ s → x ≤ a

theorem mem_lowerBounds {α : Type u} [Preorder α] {s : Set α} {a : α} : a ∈ lowerBounds s ↔ ∀ (x : α), x ∈ s → a ≤ x

theorem bddAbove_def {α : Type u} [Preorder α] {s : Set α} : BddAbove s ↔ ∃ x, ∀ (y : α), y ∈ s → y ≤ x

theorem bddBelow_def {α : Type u} [Preorder α] {s : Set α} : BddBelow s ↔ ∃ x, ∀ (y : α), y ∈ s → x ≤ y

theorem bot_mem_lowerBounds {α : Type u} [Preorder α] [OrderBot α] (s : Set α) : ⊥ ∈ lowerBounds s

theorem top_mem_upperBounds {α : Type u} [Preorder α] [OrderTop α] (s : Set α) : ⊤ ∈ upperBounds s

@[simp]

theorem isLeast_bot_iff {α : Type u} [Preorder α] {s : Set α} [OrderBot α] : IsLeast s ⊥ ↔ ⊥ ∈ s

@[simp]

theorem isGreatest_top_iff {α : Type u} [Preorder α] {s : Set α} [OrderTop α] : IsGreatest s ⊤ ↔ ⊤ ∈ s

theorem not_bddAbove_iff' {α : Type u} [Preorder α] {s : Set α} : ¬BddAbove s ↔ ∀ (x : α), ∃ y, y ∈ s ∧ ¬y ≤ x

A set s is not bounded above if and only if for each x there exists y ∈ s such that x is not greater than or equal to y. This version only assumes Preorder structure and uses ¬(y ≤ x). A version for linear orders is called not_bddAbove_iff.

theorem not_bddBelow_iff' {α : Type u} [Preorder α] {s : Set α} : ¬BddBelow s ↔ ∀ (x : α), ∃ y, y ∈ s ∧ ¬x ≤ y

A set s is not bounded below if and only if for each x there exists y ∈ s such that x is not less than or equal to y. This version only assumes Preorder structure and uses ¬(x ≤ y). A version for linear orders is called not_bddBelow_iff.

theorem not_bddAbove_iff {α : Type u_1} [LinearOrder α] {s : Set α} : ¬BddAbove s ↔ ∀ (x : α), ∃ y, y ∈ s ∧ x < y

A set s is not bounded above if and only if for each x there exists y ∈ s that is greater than x. A version for preorders is called not_bddAbove_iff'.

theorem not_bddBelow_iff {α : Type u_1} [LinearOrder α] {s : Set α} : ¬BddBelow s ↔ ∀ (x : α), ∃ y, y ∈ s ∧ y < x

A set s is not bounded below if and only if for each x there exists y ∈ s that is less than x. A version for preorders is called not_bddBelow_iff'.

theorem BddAbove.dual {α : Type u} [Preorder α] {s : Set α} (h : BddAbove s) : BddBelow (↑OrderDual.ofDual ⁻¹' s)

theorem BddBelow.dual {α : Type u} [Preorder α] {s : Set α} (h : BddBelow s) : BddAbove (↑OrderDual.ofDual ⁻¹' s)

theorem IsLeast.dual {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : IsGreatest (↑OrderDual.ofDual ⁻¹' s) (↑OrderDual.toDual a)

theorem IsGreatest.dual {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : IsLeast (↑OrderDual.ofDual ⁻¹' s) (↑OrderDual.toDual a)

theorem IsLUB.dual {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : IsGLB (↑OrderDual.ofDual ⁻¹' s) (↑OrderDual.toDual a)

theorem IsGLB.dual {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) : IsLUB (↑OrderDual.ofDual ⁻¹' s) (↑OrderDual.toDual a)

@[reducible]

def IsLeast.orderBot {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : OrderBot ↑s

If a is the least element of a set s, then subtype s is an order with bottom element.

Equations

• IsLeast.orderBot h = OrderBot.mk (_ : ∀ (x : { a // a ∈ s }), ⊥ ≤ x)

@[reducible]

def IsGreatest.orderTop {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : OrderTop ↑s

If a is the greatest element of a set s, then subtype s is an order with top element.

Equations

• IsGreatest.orderTop h = OrderTop.mk (_ : ∀ (x : { a // a ∈ s }), x ≤ ⊤)

Monotonicity

theorem upperBounds_mono_set {α : Type u} [Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (hst : s ⊆ t) : upperBounds t ⊆ upperBounds s

theorem lowerBounds_mono_set {α : Type u} [Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (hst : s ⊆ t) : lowerBounds t ⊆ lowerBounds s

theorem upperBounds_mono_mem {α : Type u} [Preorder α] {s : Set α} ⦃a : α⦄ ⦃b : α⦄ (hab : a ≤ b) : a ∈ upperBounds s → b ∈ upperBounds s

theorem lowerBounds_mono_mem {α : Type u} [Preorder α] {s : Set α} ⦃a : α⦄ ⦃b : α⦄ (hab : a ≤ b) : b ∈ lowerBounds s → a ∈ lowerBounds s

theorem upperBounds_mono {α : Type u} [Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (hst : s ⊆ t) ⦃a : α⦄ ⦃b : α⦄ (hab : a ≤ b) : a ∈ upperBounds t → b ∈ upperBounds s

theorem lowerBounds_mono {α : Type u} [Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (hst : s ⊆ t) ⦃a : α⦄ ⦃b : α⦄ (hab : a ≤ b) : b ∈ lowerBounds t → a ∈ lowerBounds s

theorem BddAbove.mono {α : Type u} [Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (h : s ⊆ t) : BddAbove t → BddAbove s

If s ⊆ t and t is bounded above, then so is s.

theorem BddBelow.mono {α : Type u} [Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (h : s ⊆ t) : BddBelow t → BddBelow s

If s ⊆ t and t is bounded below, then so is s.

theorem IsLUB.of_subset_of_superset {α : Type u} [Preorder α] {a : α} {s : Set α} {t : Set α} {p : Set α} (hs : IsLUB s a) (hp : IsLUB p a) (hst : s ⊆ t) (htp : t ⊆ p) : IsLUB t a

If a is a least upper bound for sets s and p, then it is a least upper bound for any set t, s ⊆ t ⊆ p.

theorem IsGLB.of_subset_of_superset {α : Type u} [Preorder α] {a : α} {s : Set α} {t : Set α} {p : Set α} (hs : IsGLB s a) (hp : IsGLB p a) (hst : s ⊆ t) (htp : t ⊆ p) : IsGLB t a

If a is a greatest lower bound for sets s and p, then it is a greater lower bound for any set t, s ⊆ t ⊆ p.

theorem IsLeast.mono {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} {b : α} (ha : IsLeast s a) (hb : IsLeast t b) (hst : s ⊆ t) : b ≤ a

theorem IsGreatest.mono {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} {b : α} (ha : IsGreatest s a) (hb : IsGreatest t b) (hst : s ⊆ t) : a ≤ b

theorem IsLUB.mono {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} {b : α} (ha : IsLUB s a) (hb : IsLUB t b) (hst : s ⊆ t) : a ≤ b

theorem IsGLB.mono {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} {b : α} (ha : IsGLB s a) (hb : IsGLB t b) (hst : s ⊆ t) : b ≤ a

theorem subset_lowerBounds_upperBounds {α : Type u} [Preorder α] (s : Set α) : s ⊆ lowerBounds (upperBounds s)

theorem subset_upperBounds_lowerBounds {α : Type u} [Preorder α] (s : Set α) : s ⊆ upperBounds (lowerBounds s)

theorem Set.Nonempty.bddAbove_lowerBounds {α : Type u} [Preorder α] {s : Set α} (hs : Set.Nonempty s) : BddAbove (lowerBounds s)

theorem Set.Nonempty.bddBelow_upperBounds {α : Type u} [Preorder α] {s : Set α} (hs : Set.Nonempty s) : BddBelow (upperBounds s)

Conversions

theorem IsLeast.isGLB {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : IsGLB s a

theorem IsGreatest.isLUB {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : IsLUB s a

theorem IsLUB.upperBounds_eq {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : upperBounds s = Set.Ici a

theorem IsGLB.lowerBounds_eq {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) : lowerBounds s = Set.Iic a

theorem IsLeast.lowerBounds_eq {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : lowerBounds s = Set.Iic a

theorem IsGreatest.upperBounds_eq {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : upperBounds s = Set.Ici a

theorem IsGreatest.lt_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (h : IsGreatest s a) : a < b ↔ ∀ (x : α), x ∈ s → x < b

theorem IsLeast.lt_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (h : IsLeast s a) : b < a ↔ ∀ (x : α), x ∈ s → b < x

theorem isLUB_le_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) : a ≤ b ↔ b ∈ upperBounds s

theorem le_isGLB_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) : b ≤ a ↔ b ∈ lowerBounds s

theorem isLUB_iff_le_iff {α : Type u} [Preorder α] {s : Set α} {a : α} : IsLUB s a ↔ ∀ (b : α), a ≤ b ↔ b ∈ upperBounds s

theorem isGLB_iff_le_iff {α : Type u} [Preorder α] {s : Set α} {a : α} : IsGLB s a ↔ ∀ (b : α), b ≤ a ↔ b ∈ lowerBounds s

theorem IsLUB.bddAbove {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : BddAbove s

If s has a least upper bound, then it is bounded above.

theorem IsGLB.bddBelow {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) : BddBelow s

If s has a greatest lower bound, then it is bounded below.

theorem IsGreatest.bddAbove {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : BddAbove s

If s has a greatest element, then it is bounded above.

theorem IsLeast.bddBelow {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : BddBelow s

If s has a least element, then it is bounded below.

theorem IsLeast.nonempty {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : Set.Nonempty s

theorem IsGreatest.nonempty {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : Set.Nonempty s

Union and intersection

@[simp]

theorem upperBounds_union {α : Type u} [Preorder α] {s : Set α} {t : Set α} : upperBounds (s ∪ t) = upperBounds s ∩ upperBounds t

@[simp]

theorem lowerBounds_union {α : Type u} [Preorder α] {s : Set α} {t : Set α} : lowerBounds (s ∪ t) = lowerBounds s ∩ lowerBounds t

theorem union_upperBounds_subset_upperBounds_inter {α : Type u} [Preorder α] {s : Set α} {t : Set α} : upperBounds s ∪ upperBounds t ⊆ upperBounds (s ∩ t)

theorem union_lowerBounds_subset_lowerBounds_inter {α : Type u} [Preorder α] {s : Set α} {t : Set α} : lowerBounds s ∪ lowerBounds t ⊆ lowerBounds (s ∩ t)

theorem isLeast_union_iff {α : Type u} [Preorder α] {a : α} {s : Set α} {t : Set α} : IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a

theorem isGreatest_union_iff {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} : IsGreatest (s ∪ t) a ↔ IsGreatest s a ∧ a ∈ upperBounds t ∨ a ∈ upperBounds s ∧ IsGreatest t a

theorem BddAbove.inter_of_left {α : Type u} [Preorder α] {s : Set α} {t : Set α} (h : BddAbove s) : BddAbove (s ∩ t)

If s is bounded, then so is s ∩ t

theorem BddAbove.inter_of_right {α : Type u} [Preorder α] {s : Set α} {t : Set α} (h : BddAbove t) : BddAbove (s ∩ t)

If t is bounded, then so is s ∩ t

theorem BddBelow.inter_of_left {α : Type u} [Preorder α] {s : Set α} {t : Set α} (h : BddBelow s) : BddBelow (s ∩ t)

If s is bounded, then so is s ∩ t

theorem BddBelow.inter_of_right {α : Type u} [Preorder α] {s : Set α} {t : Set α} (h : BddBelow t) : BddBelow (s ∩ t)

If t is bounded, then so is s ∩ t

theorem BddAbove.union {α : Type u} [Preorder α] [IsDirected α fun x x_1 => x ≤ x_1] {s : Set α} {t : Set α} : BddAbove s → BddAbove t → BddAbove (s ∪ t)

In a directed order, the union of bounded above sets is bounded above.

theorem bddAbove_union {α : Type u} [Preorder α] [IsDirected α fun x x_1 => x ≤ x_1] {s : Set α} {t : Set α} : BddAbove (s ∪ t) ↔ BddAbove s ∧ BddAbove t

In a directed order, the union of two sets is bounded above if and only if both sets are.

theorem BddBelow.union {α : Type u} [Preorder α] [IsDirected α fun x x_1 => x ≥ x_1] {s : Set α} {t : Set α} : BddBelow s → BddBelow t → BddBelow (s ∪ t)

In a codirected order, the union of bounded below sets is bounded below.

theorem bddBelow_union {α : Type u} [Preorder α] [IsDirected α fun x x_1 => x ≥ x_1] {s : Set α} {t : Set α} : BddBelow (s ∪ t) ↔ BddBelow s ∧ BddBelow t

In a codirected order, the union of two sets is bounded below if and only if both sets are.

theorem IsLUB.union {γ : Type w} [SemilatticeSup γ] {a : γ} {b : γ} {s : Set γ} {t : Set γ} (hs : IsLUB s a) (ht : IsLUB t b) : IsLUB (s ∪ t) (a ⊔ b)

If a is the least upper bound of s and b is the least upper bound of t, then a ⊔ b is the least upper bound of s ∪ t.

theorem IsGLB.union {γ : Type w} [SemilatticeInf γ] {a₁ : γ} {a₂ : γ} {s : Set γ} {t : Set γ} (hs : IsGLB s a₁) (ht : IsGLB t a₂) : IsGLB (s ∪ t) (a₁ ⊓ a₂)

If a is the greatest lower bound of s and b is the greatest lower bound of t, then a ⊓ b is the greatest lower bound of s ∪ t.

theorem IsLeast.union {γ : Type w} [LinearOrder γ] {a : γ} {b : γ} {s : Set γ} {t : Set γ} (ha : IsLeast s a) (hb : IsLeast t b) : IsLeast (s ∪ t) (min a b)

If a is the least element of s and b is the least element of t, then min a b is the least element of s ∪ t.

theorem IsGreatest.union {γ : Type w} [LinearOrder γ] {a : γ} {b : γ} {s : Set γ} {t : Set γ} (ha : IsGreatest s a) (hb : IsGreatest t b) : IsGreatest (s ∪ t) (max a b)

If a is the greatest element of s and b is the greatest element of t, then max a b is the greatest element of s ∪ t.

theorem IsLUB.inter_Ici_of_mem {γ : Type w} [LinearOrder γ] {s : Set γ} {a : γ} {b : γ} (ha : IsLUB s a) (hb : b ∈ s) : IsLUB (s ∩ Set.Ici b) a

theorem IsGLB.inter_Iic_of_mem {γ : Type w} [LinearOrder γ] {s : Set γ} {a : γ} {b : γ} (ha : IsGLB s a) (hb : b ∈ s) : IsGLB (s ∩ Set.Iic b) a

theorem bddAbove_iff_exists_ge {γ : Type w} [SemilatticeSup γ] {s : Set γ} (x₀ : γ) : BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ (y : γ), y ∈ s → y ≤ x

theorem bddBelow_iff_exists_le {γ : Type w} [SemilatticeInf γ] {s : Set γ} (x₀ : γ) : BddBelow s ↔ ∃ x, x ≤ x₀ ∧ ∀ (y : γ), y ∈ s → x ≤ y

theorem BddAbove.exists_ge {γ : Type w} [SemilatticeSup γ] {s : Set γ} (hs : BddAbove s) (x₀ : γ) : ∃ x, x₀ ≤ x ∧ ∀ (y : γ), y ∈ s → y ≤ x

theorem BddBelow.exists_le {γ : Type w} [SemilatticeInf γ] {s : Set γ} (hs : BddBelow s) (x₀ : γ) : ∃ x, x ≤ x₀ ∧ ∀ (y : γ), y ∈ s → x ≤ y

Specific sets

Unbounded intervals

theorem isLeast_Ici {α : Type u} [Preorder α] {a : α} : IsLeast (Set.Ici a) a

theorem isGreatest_Iic {α : Type u} [Preorder α] {a : α} : IsGreatest (Set.Iic a) a

theorem isLUB_Iic {α : Type u} [Preorder α] {a : α} : IsLUB (Set.Iic a) a

theorem isGLB_Ici {α : Type u} [Preorder α] {a : α} : IsGLB (Set.Ici a) a

theorem upperBounds_Iic {α : Type u} [Preorder α] {a : α} : upperBounds (Set.Iic a) = Set.Ici a

theorem lowerBounds_Ici {α : Type u} [Preorder α] {a : α} : lowerBounds (Set.Ici a) = Set.Iic a

theorem bddAbove_Iic {α : Type u} [Preorder α] {a : α} : BddAbove (Set.Iic a)

theorem bddBelow_Ici {α : Type u} [Preorder α] {a : α} : BddBelow (Set.Ici a)

theorem bddAbove_Iio {α : Type u} [Preorder α] {a : α} : BddAbove (Set.Iio a)

theorem bddBelow_Ioi {α : Type u} [Preorder α] {a : α} : BddBelow (Set.Ioi a)

theorem lub_Iio_le {α : Type u} [Preorder α] {b : α} (a : α) (hb : IsLUB (Set.Iio a) b) : b ≤ a

theorem le_glb_Ioi {α : Type u} [Preorder α] {b : α} (a : α) (hb : IsGLB (Set.Ioi a) b) : a ≤ b

theorem lub_Iio_eq_self_or_Iio_eq_Iic {γ : Type w} [PartialOrder γ] {j : γ} (i : γ) (hj : IsLUB (Set.Iio i) j) : j = i ∨ Set.Iio i = Set.Iic j

theorem glb_Ioi_eq_self_or_Ioi_eq_Ici {γ : Type w} [PartialOrder γ] {j : γ} (i : γ) (hj : IsGLB (Set.Ioi i) j) : j = i ∨ Set.Ioi i = Set.Ici j

theorem exists_lub_Iio {γ : Type w} [LinearOrder γ] (i : γ) : ∃ j, IsLUB (Set.Iio i) j

theorem exists_glb_Ioi {γ : Type w} [LinearOrder γ] (i : γ) : ∃ j, IsGLB (Set.Ioi i) j

theorem isLUB_Iio {γ : Type w} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : IsLUB (Set.Iio a) a

theorem isGLB_Ioi {γ : Type w} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : IsGLB (Set.Ioi a) a

theorem upperBounds_Iio {γ : Type w} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : upperBounds (Set.Iio a) = Set.Ici a

theorem lowerBounds_Ioi {γ : Type w} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : lowerBounds (Set.Ioi a) = Set.Iic a

Singleton

theorem isGreatest_singleton {α : Type u} [Preorder α] {a : α} : IsGreatest {a} a

theorem isLeast_singleton {α : Type u} [Preorder α] {a : α} : IsLeast {a} a

theorem isLUB_singleton {α : Type u} [Preorder α] {a : α} : IsLUB {a} a

theorem isGLB_singleton {α : Type u} [Preorder α] {a : α} : IsGLB {a} a

theorem bddAbove_singleton {α : Type u} [Preorder α] {a : α} : BddAbove {a}

theorem bddBelow_singleton {α : Type u} [Preorder α] {a : α} : BddBelow {a}

@[simp]

theorem upperBounds_singleton {α : Type u} [Preorder α] {a : α} : upperBounds {a} = Set.Ici a

@[simp]

theorem lowerBounds_singleton {α : Type u} [Preorder α] {a : α} : lowerBounds {a} = Set.Iic a

Bounded intervals

theorem bddAbove_Icc {α : Type u} [Preorder α] {a : α} {b : α} : BddAbove (Set.Icc a b)

theorem bddBelow_Icc {α : Type u} [Preorder α] {a : α} {b : α} : BddBelow (Set.Icc a b)

theorem bddAbove_Ico {α : Type u} [Preorder α] {a : α} {b : α} : BddAbove (Set.Ico a b)

theorem bddBelow_Ico {α : Type u} [Preorder α] {a : α} {b : α} : BddBelow (Set.Ico a b)

theorem bddAbove_Ioc {α : Type u} [Preorder α] {a : α} {b : α} : BddAbove (Set.Ioc a b)

theorem bddBelow_Ioc {α : Type u} [Preorder α] {a : α} {b : α} : BddBelow (Set.Ioc a b)

theorem bddAbove_Ioo {α : Type u} [Preorder α] {a : α} {b : α} : BddAbove (Set.Ioo a b)

theorem bddBelow_Ioo {α : Type u} [Preorder α] {a : α} {b : α} : BddBelow (Set.Ioo a b)

theorem isGreatest_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) : IsGreatest (Set.Icc a b) b

theorem isLUB_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) : IsLUB (Set.Icc a b) b

theorem upperBounds_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) : upperBounds (Set.Icc a b) = Set.Ici b

theorem isLeast_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) : IsLeast (Set.Icc a b) a

theorem isGLB_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) : IsGLB (Set.Icc a b) a

theorem lowerBounds_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) : lowerBounds (Set.Icc a b) = Set.Iic a

theorem isGreatest_Ioc {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : IsGreatest (Set.Ioc a b) b

theorem isLUB_Ioc {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : IsLUB (Set.Ioc a b) b

theorem upperBounds_Ioc {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : upperBounds (Set.Ioc a b) = Set.Ici b

theorem isLeast_Ico {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : IsLeast (Set.Ico a b) a

theorem isGLB_Ico {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : IsGLB (Set.Ico a b) a

theorem lowerBounds_Ico {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : lowerBounds (Set.Ico a b) = Set.Iic a

theorem isGLB_Ioo {γ : Type w} [SemilatticeSup γ] [DenselyOrdered γ] {a : γ} {b : γ} (h : a < b) : IsGLB (Set.Ioo a b) a

theorem lowerBounds_Ioo {γ : Type w} [SemilatticeSup γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : lowerBounds (Set.Ioo a b) = Set.Iic a

theorem isGLB_Ioc {γ : Type w} [SemilatticeSup γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : IsGLB (Set.Ioc a b) a

theorem lowerBounds_Ioc {γ : Type w} [SemilatticeSup γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : lowerBounds (Set.Ioc a b) = Set.Iic a

theorem isLUB_Ioo {γ : Type w} [SemilatticeInf γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : IsLUB (Set.Ioo a b) b

theorem upperBounds_Ioo {γ : Type w} [SemilatticeInf γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : upperBounds (Set.Ioo a b) = Set.Ici b

theorem isLUB_Ico {γ : Type w} [SemilatticeInf γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : IsLUB (Set.Ico a b) b

theorem upperBounds_Ico {γ : Type w} [SemilatticeInf γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) : upperBounds (Set.Ico a b) = Set.Ici b

theorem bddBelow_iff_subset_Ici {α : Type u} [Preorder α] {s : Set α} : BddBelow s ↔ ∃ a, s ⊆ Set.Ici a

theorem bddAbove_iff_subset_Iic {α : Type u} [Preorder α] {s : Set α} : BddAbove s ↔ ∃ a, s ⊆ Set.Iic a

theorem bddBelow_bddAbove_iff_subset_Icc {α : Type u} [Preorder α] {s : Set α} : BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Set.Icc a b

Univ

@[simp]

theorem isGreatest_univ_iff {α : Type u} [Preorder α] {a : α} : IsGreatest Set.univ a ↔ IsTop a

theorem isGreatest_univ {α : Type u} [Preorder α] [OrderTop α] : IsGreatest Set.univ ⊤

@[simp]

theorem OrderTop.upperBounds_univ {γ : Type w} [PartialOrder γ] [OrderTop γ] : upperBounds Set.univ = {⊤}

theorem isLUB_univ {α : Type u} [Preorder α] [OrderTop α] : IsLUB Set.univ ⊤

@[simp]

theorem OrderBot.lowerBounds_univ {γ : Type w} [PartialOrder γ] [OrderBot γ] : lowerBounds Set.univ = {⊥}

@[simp]

theorem isLeast_univ_iff {α : Type u} [Preorder α] {a : α} : IsLeast Set.univ a ↔ IsBot a

theorem isLeast_univ {α : Type u} [Preorder α] [OrderBot α] : IsLeast Set.univ ⊥

theorem isGLB_univ {α : Type u} [Preorder α] [OrderBot α] : IsGLB Set.univ ⊥

@[simp]

theorem NoMaxOrder.upperBounds_univ {α : Type u} [Preorder α] [NoMaxOrder α] : upperBounds Set.univ = ∅

@[simp]

theorem NoMinOrder.lowerBounds_univ {α : Type u} [Preorder α] [NoMinOrder α] : lowerBounds Set.univ = ∅

@[simp]

theorem not_bddAbove_univ {α : Type u} [Preorder α] [NoMaxOrder α] : ¬BddAbove Set.univ

@[simp]

theorem not_bddBelow_univ {α : Type u} [Preorder α] [NoMinOrder α] : ¬BddBelow Set.univ

Empty set

@[simp]

theorem upperBounds_empty {α : Type u} [Preorder α] : upperBounds ∅ = Set.univ

@[simp]

theorem lowerBounds_empty {α : Type u} [Preorder α] : lowerBounds ∅ = Set.univ

@[simp]

theorem bddAbove_empty {α : Type u} [Preorder α] [Nonempty α] : BddAbove ∅

@[simp]

theorem bddBelow_empty {α : Type u} [Preorder α] [Nonempty α] : BddBelow ∅

@[simp]

theorem isGLB_empty_iff {α : Type u} [Preorder α] {a : α} : IsGLB ∅ a ↔ IsTop a

@[simp]

theorem isLUB_empty_iff {α : Type u} [Preorder α] {a : α} : IsLUB ∅ a ↔ IsBot a

theorem isGLB_empty {α : Type u} [Preorder α] [OrderTop α] : IsGLB ∅ ⊤

theorem isLUB_empty {α : Type u} [Preorder α] [OrderBot α] : IsLUB ∅ ⊥

theorem IsLUB.nonempty {α : Type u} [Preorder α] {s : Set α} {a : α} [NoMinOrder α] (hs : IsLUB s a) : Set.Nonempty s

theorem IsGLB.nonempty {α : Type u} [Preorder α] {s : Set α} {a : α} [NoMaxOrder α] (hs : IsGLB s a) : Set.Nonempty s

theorem nonempty_of_not_bddAbove {α : Type u} [Preorder α] {s : Set α} [ha : Nonempty α] (h : ¬BddAbove s) : Set.Nonempty s

theorem nonempty_of_not_bddBelow {α : Type u} [Preorder α] {s : Set α} [Nonempty α] (h : ¬BddBelow s) : Set.Nonempty s

insert

@[simp]

theorem bddAbove_insert {α : Type u} [Preorder α] [IsDirected α fun x x_1 => x ≤ x_1] {s : Set α} {a : α} : BddAbove (insert a s) ↔ BddAbove s

Adding a point to a set preserves its boundedness above.

theorem BddAbove.insert {α : Type u} [Preorder α] [IsDirected α fun x x_1 => x ≤ x_1] {s : Set α} (a : α) : BddAbove s → BddAbove (insert a s)

@[simp]

theorem bddBelow_insert {α : Type u} [Preorder α] [IsDirected α fun x x_1 => x ≥ x_1] {s : Set α} {a : α} : BddBelow (insert a s) ↔ BddBelow s

Adding a point to a set preserves its boundedness below.

theorem BddBelow.insert {α : Type u} [Preorder α] [IsDirected α fun x x_1 => x ≥ x_1] {s : Set α} (a : α) : BddBelow s → BddBelow (insert a s)

theorem IsLUB.insert {γ : Type w} [SemilatticeSup γ] (a : γ) {b : γ} {s : Set γ} (hs : IsLUB s b) : IsLUB (insert a s) (a ⊔ b)

theorem IsGLB.insert {γ : Type w} [SemilatticeInf γ] (a : γ) {b : γ} {s : Set γ} (hs : IsGLB s b) : IsGLB (insert a s) (a ⊓ b)

theorem IsGreatest.insert {γ : Type w} [LinearOrder γ] (a : γ) {b : γ} {s : Set γ} (hs : IsGreatest s b) : IsGreatest (insert a s) (max a b)

theorem IsLeast.insert {γ : Type w} [LinearOrder γ] (a : γ) {b : γ} {s : Set γ} (hs : IsLeast s b) : IsLeast (insert a s) (min a b)

@[simp]

theorem upperBounds_insert {α : Type u} [Preorder α] (a : α) (s : Set α) : upperBounds (insert a s) = Set.Ici a ∩ upperBounds s

@[simp]

theorem lowerBounds_insert {α : Type u} [Preorder α] (a : α) (s : Set α) : lowerBounds (insert a s) = Set.Iic a ∩ lowerBounds s

@[simp]

theorem OrderTop.bddAbove {α : Type u} [Preorder α] [OrderTop α] (s : Set α) : BddAbove s

When there is a global maximum, every set is bounded above.

@[simp]

theorem OrderBot.bddBelow {α : Type u} [Preorder α] [OrderBot α] (s : Set α) : BddBelow s

When there is a global minimum, every set is bounded below.

def tacticBddDefault : Lean.ParserDescr

Sets are automatically bounded or cobounded in complete lattices. To use the same statements in complete and conditionally complete lattices but let automation fill automatically the boundedness proofs in complete lattices, we use the tactic bddDefault in the statements, in the form (hA : BddAbove A := by bddDefault).

Equations

• tacticBddDefault = Lean.ParserDescr.node `tacticBddDefault 1024 (Lean.ParserDescr.nonReservedSymbol "bddDefault" false)

Pair

theorem isLUB_pair {γ : Type w} [SemilatticeSup γ] {a : γ} {b : γ} : IsLUB {a, b} (a ⊔ b)

theorem isGLB_pair {γ : Type w} [SemilatticeInf γ] {a : γ} {b : γ} : IsGLB {a, b} (a ⊓ b)

theorem isLeast_pair {γ : Type w} [LinearOrder γ] {a : γ} {b : γ} : IsLeast {a, b} (min a b)

theorem isGreatest_pair {γ : Type w} [LinearOrder γ] {a : γ} {b : γ} : IsGreatest {a, b} (max a b)

Lower/upper bounds

@[simp]

theorem isLUB_lowerBounds {α : Type u} [Preorder α] {s : Set α} {a : α} : IsLUB (lowerBounds s) a ↔ IsGLB s a

@[simp]

theorem isGLB_upperBounds {α : Type u} [Preorder α] {s : Set α} {a : α} : IsGLB (upperBounds s) a ↔ IsLUB s a

(In)equalities with the least upper bound and the greatest lower bound

theorem lowerBounds_le_upperBounds {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s) : Set.Nonempty s → a ≤ b

theorem isGLB_le_isLUB {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (ha : IsGLB s a) (hb : IsLUB s b) (hs : Set.Nonempty s) : a ≤ b

theorem isLUB_lt_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (ha : IsLUB s a) : a < b ↔ ∃ c, c ∈ upperBounds s ∧ c < b

theorem lt_isGLB_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (ha : IsGLB s a) : b < a ↔ ∃ c, c ∈ lowerBounds s ∧ b < c

theorem le_of_isLUB_le_isGLB {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} {x : α} {y : α} (ha : IsGLB s a) (hb : IsLUB s b) (hab : b ≤ a) (hx : x ∈ s) (hy : y ∈ s) : x ≤ y

theorem IsLeast.unique {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsLeast s a) (Hb : IsLeast s b) : a = b

theorem IsLeast.isLeast_iff_eq {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsLeast s a) : IsLeast s b ↔ a = b

theorem IsGreatest.unique {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGreatest s a) (Hb : IsGreatest s b) : a = b

theorem IsGreatest.isGreatest_iff_eq {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGreatest s a) : IsGreatest s b ↔ a = b

theorem IsLUB.unique {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsLUB s a) (Hb : IsLUB s b) : a = b

theorem IsGLB.unique {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGLB s a) (Hb : IsGLB s b) : a = b

theorem Set.subsingleton_of_isLUB_le_isGLB {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGLB s a) (Hb : IsLUB s b) (hab : b ≤ a) : Set.Subsingleton s

theorem isGLB_lt_isLUB_of_ne {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGLB s a) (Hb : IsLUB s b) {x : α} {y : α} (Hx : x ∈ s) (Hy : y ∈ s) (Hxy : x ≠ y) : a < b

theorem lt_isLUB_iff {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) : b < a ↔ ∃ c, c ∈ s ∧ b < c

theorem isGLB_lt_iff {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) : a < b ↔ ∃ c, c ∈ s ∧ c < b

theorem IsLUB.exists_between {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) (hb : b < a) : ∃ c, c ∈ s ∧ b < c ∧ c ≤ a

theorem IsLUB.exists_between' {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) (h' : ¬a ∈ s) (hb : b < a) : ∃ c, c ∈ s ∧ b < c ∧ c < a

theorem IsGLB.exists_between {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) (hb : a < b) : ∃ c, c ∈ s ∧ a ≤ c ∧ c < b

theorem IsGLB.exists_between' {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) (h' : ¬a ∈ s) (hb : a < b) : ∃ c, c ∈ s ∧ a < c ∧ c < b

Images of upper/lower bounds under monotone functions

theorem MonotoneOn.mem_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) {a : α} (Hst : s ⊆ t) (Has : a ∈ upperBounds s) (Hat : a ∈ t) : f a ∈ upperBounds (f '' s)

theorem MonotoneOn.mem_upperBounds_image_self {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} (Hf : MonotoneOn f t) {a : α} : a ∈ upperBounds t → a ∈ t → f a ∈ upperBounds (f '' t)

theorem MonotoneOn.mem_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) {a : α} (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) (Hat : a ∈ t) : f a ∈ lowerBounds (f '' s)

theorem MonotoneOn.mem_lowerBounds_image_self {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} (Hf : MonotoneOn f t) {a : α} : a ∈ lowerBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)

theorem MonotoneOn.image_upperBounds_subset_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)

theorem MonotoneOn.image_lowerBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : f '' (lowerBounds s ∩ t) ⊆ lowerBounds (f '' s)

theorem MonotoneOn.map_bddAbove {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : Set.Nonempty (upperBounds s ∩ t) → BddAbove (f '' s)

The image under a monotone function on a set t of a subset which has an upper bound in t is bounded above.

theorem MonotoneOn.map_bddBelow {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : Set.Nonempty (lowerBounds s ∩ t) → BddBelow (f '' s)

The image under a monotone function on a set t of a subset which has a lower bound in t is bounded below.

theorem MonotoneOn.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} (Hf : MonotoneOn f t) {a : α} (Ha : IsLeast t a) : IsLeast (f '' t) (f a)

A monotone map sends a least element of a set to a least element of its image.

theorem MonotoneOn.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} (Hf : MonotoneOn f t) {a : α} (Ha : IsGreatest t a) : IsGreatest (f '' t) (f a)

A monotone map sends a greatest element of a set to a greatest element of its image.

theorem AntitoneOn.mem_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) {a : α} (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) : a ∈ t → f a ∈ upperBounds (f '' s)

theorem AntitoneOn.mem_upperBounds_image_self {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} (Hf : AntitoneOn f t) {a : α} : a ∈ lowerBounds t → a ∈ t → f a ∈ upperBounds (f '' t)

theorem AntitoneOn.mem_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) {a : α} (Hst : s ⊆ t) : a ∈ upperBounds s → a ∈ t → f a ∈ lowerBounds (f '' s)

theorem AntitoneOn.mem_lowerBounds_image_self {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} (Hf : AntitoneOn f t) {a : α} : a ∈ upperBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)

theorem AntitoneOn.image_lowerBounds_subset_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : f '' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s)

theorem AntitoneOn.image_upperBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : f '' (upperBounds s ∩ t) ⊆ lowerBounds (f '' s)

theorem AntitoneOn.map_bddAbove {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : Set.Nonempty (upperBounds s ∩ t) → BddBelow (f '' s)

The image under an antitone function of a set which is bounded above is bounded below.

theorem AntitoneOn.map_bddBelow {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : Set.Nonempty (lowerBounds s ∩ t) → BddAbove (f '' s)

The image under an antitone function of a set which is bounded below is bounded above.

theorem AntitoneOn.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} (Hf : AntitoneOn f t) {a : α} : IsGreatest t a → IsLeast (f '' t) (f a)

An antitone map sends a greatest element of a set to a least element of its image.

theorem AntitoneOn.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} (Hf : AntitoneOn f t) {a : α} : IsLeast t a → IsGreatest (f '' t) (f a)

An antitone map sends a least element of a set to a greatest element of its image.

theorem Monotone.mem_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {a : α} {s : Set α} (Ha : a ∈ upperBounds s) : f a ∈ upperBounds (f '' s)

theorem Monotone.mem_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {a : α} {s : Set α} (Ha : a ∈ lowerBounds s) : f a ∈ lowerBounds (f '' s)

theorem Monotone.image_upperBounds_subset_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {s : Set α} : f '' upperBounds s ⊆ upperBounds (f '' s)

theorem Monotone.image_lowerBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {s : Set α} : f '' lowerBounds s ⊆ lowerBounds (f '' s)

theorem Monotone.map_bddAbove {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {s : Set α} : BddAbove s → BddAbove (f '' s)

The image under a monotone function of a set which is bounded above is bounded above. See also BddAbove.image2.

theorem Monotone.map_bddBelow {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {s : Set α} : BddBelow s → BddBelow (f '' s)

The image under a monotone function of a set which is bounded below is bounded below. See also BddBelow.image2.

theorem Monotone.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {a : α} {s : Set α} (Ha : IsLeast s a) : IsLeast (f '' s) (f a)

A monotone map sends a least element of a set to a least element of its image.

theorem Monotone.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {a : α} {s : Set α} (Ha : IsGreatest s a) : IsGreatest (f '' s) (f a)

A monotone map sends a greatest element of a set to a greatest element of its image.

theorem Antitone.mem_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {a : α} {s : Set α} : a ∈ lowerBounds s → f a ∈ upperBounds (f '' s)

theorem Antitone.mem_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {a : α} {s : Set α} : a ∈ upperBounds s → f a ∈ lowerBounds (f '' s)

theorem Antitone.image_lowerBounds_subset_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {s : Set α} : f '' lowerBounds s ⊆ upperBounds (f '' s)

theorem Antitone.image_upperBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {s : Set α} : f '' upperBounds s ⊆ lowerBounds (f '' s)

theorem Antitone.map_bddAbove {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {s : Set α} : BddAbove s → BddBelow (f '' s)

The image under an antitone function of a set which is bounded above is bounded below.

theorem Antitone.map_bddBelow {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {s : Set α} : BddBelow s → BddAbove (f '' s)

The image under an antitone function of a set which is bounded below is bounded above.

theorem Antitone.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {a : α} {s : Set α} : IsGreatest s a → IsLeast (f '' s) (f a)

An antitone map sends a greatest element of a set to a least element of its image.

theorem Antitone.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {a : α} {s : Set α} : IsLeast s a → IsGreatest (f '' s) (f a)

An antitone map sends a least element of a set to a greatest element of its image.

theorem mem_upperBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (Set.image2 f s t)

theorem mem_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)

theorem image2_upperBounds_upperBounds_subset {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (Set.image2 f s t)

theorem image2_lowerBounds_lowerBounds_subset {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (Set.image2 f s t)

theorem BddAbove.image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : BddAbove s → BddAbove t → BddAbove (Set.image2 f s t)

See also Monotone.map_bddAbove.

theorem BddBelow.image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : BddBelow s → BddBelow t → BddBelow (Set.image2 f s t)

See also Monotone.map_bddBelow.

theorem IsGreatest.image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsGreatest s a) (hb : IsGreatest t b) : IsGreatest (Set.image2 f s t) (f a b)

theorem IsLeast.image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsLeast s a) (hb : IsLeast t b) : IsLeast (Set.image2 f s t) (f a b)

theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (Set.image2 f s t)

theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)

theorem image2_upperBounds_lowerBounds_subset_upperBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (Set.image2 f s t)

theorem image2_lowerBounds_upperBounds_subset_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (Set.image2 f s t)

theorem BddAbove.bddAbove_image2_of_bddBelow {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : BddAbove s → BddBelow t → BddAbove (Set.image2 f s t)

theorem BddBelow.bddBelow_image2_of_bddAbove {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : BddBelow s → BddAbove t → BddBelow (Set.image2 f s t)

theorem IsGreatest.isGreatest_image2_of_isLeast {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsGreatest s a) (hb : IsLeast t b) : IsGreatest (Set.image2 f s t) (f a b)

theorem IsLeast.isLeast_image2_of_isGreatest {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsLeast s a) (hb : IsGreatest t b) : IsLeast (Set.image2 f s t) (f a b)

theorem mem_upperBounds_image2_of_mem_lowerBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (Set.image2 f s t)

theorem mem_lowerBounds_image2_of_mem_upperBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)

theorem image2_upperBounds_upperBounds_subset_upperBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (Set.image2 f s t)

theorem image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (Set.image2 f s t)

theorem BddBelow.image2_bddAbove {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : BddBelow s → BddBelow t → BddAbove (Set.image2 f s t)

theorem BddAbove.image2_bddBelow {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : BddAbove s → BddAbove t → BddBelow (Set.image2 f s t)

theorem IsLeast.isGreatest_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsLeast s a) (hb : IsLeast t b) : IsGreatest (Set.image2 f s t) (f a b)

theorem IsGreatest.isLeast_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsGreatest s a) (hb : IsGreatest t b) : IsLeast (Set.image2 f s t) (f a b)

theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (Set.image2 f s t)

theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)

theorem image2_lowerBounds_upperBounds_subset_upperBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (Set.image2 f s t)

theorem image2_upperBounds_lowerBounds_subset_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (upperBounds s) (lowerBounds t) ⊆ lowerBounds (Set.image2 f s t)

theorem BddBelow.bddAbove_image2_of_bddAbove {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : BddBelow s → BddAbove t → BddAbove (Set.image2 f s t)

theorem BddAbove.bddBelow_image2_of_bddAbove {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : BddAbove s → BddBelow t → BddBelow (Set.image2 f s t)

theorem IsLeast.isGreatest_image2_of_isGreatest {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsLeast s a) (hb : IsGreatest t b) : IsGreatest (Set.image2 f s t) (f a b)

theorem IsGreatest.isLeast_image2_of_isLeast {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsGreatest s a) (hb : IsLeast t b) : IsLeast (Set.image2 f s t) (f a b)

theorem bddAbove_pi {α : Type u} {π : α → Type u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} : BddAbove s ↔ ∀ (a : α), BddAbove (Function.eval a '' s)

theorem bddBelow_pi {α : Type u} {π : α → Type u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} : BddBelow s ↔ ∀ (a : α), BddBelow (Function.eval a '' s)

theorem bddAbove_range_pi {α : Type u} {ι : Sort x} {π : α → Type u_1} [(a : α) → Preorder (π a)] {F : ι → (a : α) → π a} : BddAbove (Set.range F) ↔ ∀ (a : α), BddAbove (Set.range fun i => F i a)

theorem bddBelow_range_pi {α : Type u} {ι : Sort x} {π : α → Type u_1} [(a : α) → Preorder (π a)] {F : ι → (a : α) → π a} : BddBelow (Set.range F) ↔ ∀ (a : α), BddBelow (Set.range fun i => F i a)

theorem isLUB_pi {α : Type u} {π : α → Type u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} {f : (a : α) → π a} : IsLUB s f ↔ ∀ (a : α), IsLUB (Function.eval a '' s) (f a)

theorem isGLB_pi {α : Type u} {π : α → Type u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} {f : (a : α) → π a} : IsGLB s f ↔ ∀ (a : α), IsGLB (Function.eval a '' s) (f a)

theorem IsGLB.of_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) {s : Set α} {x : α} (hx : IsGLB (f '' s) (f x)) : IsGLB s x

theorem IsLUB.of_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) {s : Set α} {x : α} (hx : IsLUB (f '' s) (f x)) : IsLUB s x

theorem isLUB_prod {α : Type u} {β : Type v} [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × β) : IsLUB s p ↔ IsLUB (Prod.fst '' s) p.fst ∧ IsLUB (Prod.snd '' s) p.snd

theorem isGLB_prod {α : Type u} {β : Type v} [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × β) : IsGLB s p ↔ IsGLB (Prod.fst '' s) p.fst ∧ IsGLB (Prod.snd '' s) p.snd

def ScottContinuous {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) : Prop

A function between preorders is said to be Scott continuous if it preserves IsLUB on directed sets. It can be shown that a function is Scott continuous if and only if it is continuous wrt the Scott topology.

The dual notion

∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≥ ·) d → ∀ ⦃a⦄, IsGLB d a → IsGLB (f '' d) (f a)

does not appear to play a significant role in the literature, so is omitted here.

Equations

• ScottContinuous f = ∀ ⦃d : Set α⦄, Set.Nonempty d → DirectedOn (fun x x_1 => x ≤ x_1) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)

theorem ScottContinuous.monotone {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (h : ScottContinuous f) : Monotone f