mathlib3 documentation

order.bounds.basic

Upper / lower bounds #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define:

We also prove various lemmas about monotonicity, behaviour under ∪, ∩, insert, and provide formulas for ∅, univ, and intervals.

Definitions #

source
def upper_bounds {α : Type u} [preorder α] (s : set α) :
set α

The set of upper bounds of a set.

Equations
source
def lower_bounds {α : Type u} [preorder α] (s : set α) :
set α

The set of lower bounds of a set.

Equations
source
def bdd_above {α : Type u} [preorder α] (s : set α) :
Prop

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

Equations
source
def bdd_below {α : Type u} [preorder α] (s : set α) :
Prop

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

Equations
source
def is_least {α : 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
source
def is_greatest {α : 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
source
def is_lub {α : 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
source
def is_glb {α : 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
source
theorem mem_upper_bounds {α : Type u} [preorder α] {s : set α} {a : α} :
a ∈ upper_bounds s ↔ ∀ (x : α), x ∈ s → x ≤ a
source
theorem mem_lower_bounds {α : Type u} [preorder α] {s : set α} {a : α} :
a ∈ lower_bounds s ↔ ∀ (x : α), x ∈ s → a ≤ x
source
theorem mem_upper_bounds_iff_subset_Iic {α : Type u} [preorder α] {s : set α} {a : α} :
a ∈ upper_bounds s ↔ s ⊆ set.Iic a
source
theorem mem_lower_bounds_iff_subset_Ici {α : Type u} [preorder α] {s : set α} {a : α} :
a ∈ lower_bounds s ↔ s ⊆ set.Ici a
source
theorem bdd_above_def {α : Type u} [preorder α] {s : set α} :
bdd_above s ↔ ∃ (x : α), ∀ (y : α), y ∈ s → y ≤ x
source
theorem bdd_below_def {α : Type u} [preorder α] {s : set α} :
bdd_below s ↔ ∃ (x : α), ∀ (y : α), y ∈ s → x ≤ y
source
theorem bot_mem_lower_bounds {α : Type u} [preorder α] [order_bot α] (s : set α) :
⊥ ∈ lower_bounds s
source
theorem top_mem_upper_bounds {α : Type u} [preorder α] [order_top α] (s : set α) :
⊤ ∈ upper_bounds s
source
@[simp]
theorem is_least_bot_iff {α : Type u} [preorder α] {s : set α} [order_bot α] :
is_least s ⊥ ↔ ⊥ ∈ s
source
@[simp]
theorem is_greatest_top_iff {α : Type u} [preorder α] {s : set α} [order_top α] :
is_greatest s ⊤ ↔ ⊤ ∈ s
source
theorem not_bdd_above_iff' {α : Type u} [preorder α] {s : set α} :
¬bdd_above s ↔ ∀ (x : α), ∃ (y : α) (H : 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_bdd_above_iff.

source
theorem not_bdd_below_iff' {α : Type u} [preorder α] {s : set α} :
¬bdd_below s ↔ ∀ (x : α), ∃ (y : α) (H : 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_bdd_below_iff.

source
theorem not_bdd_above_iff {α : Type u_1} [linear_order α] {s : set α} :
¬bdd_above s ↔ ∀ (x : α), ∃ (y : α) (H : 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_bdd_above_iff'.

source
theorem not_bdd_below_iff {α : Type u_1} [linear_order α] {s : set α} :
¬bdd_below s ↔ ∀ (x : α), ∃ (y : α) (H : 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_bdd_below_iff'.

source
theorem bdd_above.dual {α : Type u} [preorder α] {s : set α} (h : bdd_above s) :
bdd_below (⇑order_dual.of_dual ⁻¹' s)
source
theorem bdd_below.dual {α : Type u} [preorder α] {s : set α} (h : bdd_below s) :
bdd_above (⇑order_dual.of_dual ⁻¹' s)
source
theorem is_least.dual {α : Type u} [preorder α] {s : set α} {a : α} (h : is_least s a) :
is_greatest (⇑order_dual.of_dual ⁻¹' s) (⇑order_dual.to_dual a)
source
theorem is_greatest.dual {α : Type u} [preorder α] {s : set α} {a : α} (h : is_greatest s a) :
is_least (⇑order_dual.of_dual ⁻¹' s) (⇑order_dual.to_dual a)
source
theorem is_lub.dual {α : Type u} [preorder α] {s : set α} {a : α} (h : is_lub s a) :
is_glb (⇑order_dual.of_dual ⁻¹' s) (⇑order_dual.to_dual a)
source
theorem is_glb.dual {α : Type u} [preorder α] {s : set α} {a : α} (h : is_glb s a) :
is_lub (⇑order_dual.of_dual ⁻¹' s) (⇑order_dual.to_dual a)
source
@[reducible]
def is_least.order_bot {α : Type u} [preorder α] {s : set α} {a : α} (h : is_least s a) :
order_bot ↥s

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

Equations
source
@[reducible]
def is_greatest.order_top {α : Type u} [preorder α] {s : set α} {a : α} (h : is_greatest s a) :
order_top ↥s

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

Equations

Monotonicity #

source
theorem upper_bounds_mono_set {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s ⊆ t) :
upper_bounds t ⊆ upper_bounds s
source
theorem lower_bounds_mono_set {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s ⊆ t) :
lower_bounds t ⊆ lower_bounds s
source
theorem upper_bounds_mono_mem {α : Type u} [preorder α] {s : set α} ⦃a b : α⦄ (hab : a ≤ b) :
a ∈ upper_bounds s → b ∈ upper_bounds s
source
theorem lower_bounds_mono_mem {α : Type u} [preorder α] {s : set α} ⦃a b : α⦄ (hab : a ≤ b) :
b ∈ lower_bounds s → a ∈ lower_bounds s
source
theorem upper_bounds_mono {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s ⊆ t) ⦃a b : α⦄ (hab : a ≤ b) :
a ∈ upper_bounds t → b ∈ upper_bounds s
source
theorem lower_bounds_mono {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s ⊆ t) ⦃a b : α⦄ (hab : a ≤ b) :
b ∈ lower_bounds t → a ∈ lower_bounds s
source
theorem bdd_above.mono {α : Type u} [preorder α] ⦃s t : set α⦄ (h : s ⊆ t) :
bdd_above t → bdd_above s

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

source
theorem bdd_below.mono {α : Type u} [preorder α] ⦃s t : set α⦄ (h : s ⊆ t) :
bdd_below t → bdd_below s

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

source
theorem is_lub.of_subset_of_superset {α : Type u} [preorder α] {a : α} {s t p : set α} (hs : is_lub s a) (hp : is_lub p a) (hst : s ⊆ t) (htp : t ⊆ p) :
is_lub 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.

source
theorem is_glb.of_subset_of_superset {α : Type u} [preorder α] {a : α} {s t p : set α} (hs : is_glb s a) (hp : is_glb p a) (hst : s ⊆ t) (htp : t ⊆ p) :
is_glb 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.

source
theorem is_least.mono {α : Type u} [preorder α] {s t : set α} {a b : α} (ha : is_least s a) (hb : is_least t b) (hst : s ⊆ t) :
b ≤ a
source
theorem is_greatest.mono {α : Type u} [preorder α] {s t : set α} {a b : α} (ha : is_greatest s a) (hb : is_greatest t b) (hst : s ⊆ t) :
a ≤ b
source
theorem is_lub.mono {α : Type u} [preorder α] {s t : set α} {a b : α} (ha : is_lub s a) (hb : is_lub t b) (hst : s ⊆ t) :
a ≤ b
source
theorem is_glb.mono {α : Type u} [preorder α] {s t : set α} {a b : α} (ha : is_glb s a) (hb : is_glb t b) (hst : s ⊆ t) :
b ≤ a
source
theorem subset_lower_bounds_upper_bounds {α : Type u} [preorder α] (s : set α) :
s ⊆ lower_bounds (upper_bounds s)
source
theorem subset_upper_bounds_lower_bounds {α : Type u} [preorder α] (s : set α) :
s ⊆ upper_bounds (lower_bounds s)
source
theorem set.nonempty.bdd_above_lower_bounds {α : Type u} [preorder α] {s : set α} (hs : s.nonempty) :
bdd_above (lower_bounds s)
source
theorem set.nonempty.bdd_below_upper_bounds {α : Type u} [preorder α] {s : set α} (hs : s.nonempty) :
bdd_below (upper_bounds s)

Conversions #

source
theorem is_least.is_glb {α : Type u} [preorder α] {s : set α} {a : α} (h : is_least s a) :
is_glb s a
source
theorem is_greatest.is_lub {α : Type u} [preorder α] {s : set α} {a : α} (h : is_greatest s a) :
is_lub s a
source
theorem is_lub.upper_bounds_eq {α : Type u} [preorder α] {s : set α} {a : α} (h : is_lub s a) :
upper_bounds s = set.Ici a
source
theorem is_glb.lower_bounds_eq {α : Type u} [preorder α] {s : set α} {a : α} (h : is_glb s a) :
lower_bounds s = set.Iic a
source
theorem is_least.lower_bounds_eq {α : Type u} [preorder α] {s : set α} {a : α} (h : is_least s a) :
lower_bounds s = set.Iic a
source
theorem is_greatest.upper_bounds_eq {α : Type u} [preorder α] {s : set α} {a : α} (h : is_greatest s a) :
upper_bounds s = set.Ici a
source
theorem is_lub_le_iff {α : Type u} [preorder α] {s : set α} {a b : α} (h : is_lub s a) :
a ≤ b ↔ b ∈ upper_bounds s
source
theorem le_is_glb_iff {α : Type u} [preorder α] {s : set α} {a b : α} (h : is_glb s a) :
b ≤ a ↔ b ∈ lower_bounds s
source
theorem is_lub_iff_le_iff {α : Type u} [preorder α] {s : set α} {a : α} :
is_lub s a ↔ ∀ (b : α), a ≤ b ↔ b ∈ upper_bounds s
source
theorem is_glb_iff_le_iff {α : Type u} [preorder α] {s : set α} {a : α} :
is_glb s a ↔ ∀ (b : α), b ≤ a ↔ b ∈ lower_bounds s
source
theorem is_lub.bdd_above {α : Type u} [preorder α] {s : set α} {a : α} (h : is_lub s a) :
bdd_above s

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

source
theorem is_glb.bdd_below {α : Type u} [preorder α] {s : set α} {a : α} (h : is_glb s a) :
bdd_below s

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

source
theorem is_greatest.bdd_above {α : Type u} [preorder α] {s : set α} {a : α} (h : is_greatest s a) :
bdd_above s

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

source
theorem is_least.bdd_below {α : Type u} [preorder α] {s : set α} {a : α} (h : is_least s a) :
bdd_below s

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

source
theorem is_least.nonempty {α : Type u} [preorder α] {s : set α} {a : α} (h : is_least s a) :
s.nonempty
source
theorem is_greatest.nonempty {α : Type u} [preorder α] {s : set α} {a : α} (h : is_greatest s a) :
s.nonempty

Union and intersection #

source
@[simp]
theorem upper_bounds_union {α : Type u} [preorder α] {s t : set α} :
upper_bounds (s ∪ t) = upper_bounds s ∩ upper_bounds t
source
@[simp]
theorem lower_bounds_union {α : Type u} [preorder α] {s t : set α} :
lower_bounds (s ∪ t) = lower_bounds s ∩ lower_bounds t
source
theorem union_upper_bounds_subset_upper_bounds_inter {α : Type u} [preorder α] {s t : set α} :
upper_bounds s ∪ upper_bounds t ⊆ upper_bounds (s ∩ t)
source
theorem union_lower_bounds_subset_lower_bounds_inter {α : Type u} [preorder α] {s t : set α} :
lower_bounds s ∪ lower_bounds t ⊆ lower_bounds (s ∩ t)
source
theorem is_least_union_iff {α : Type u} [preorder α] {a : α} {s t : set α} :
is_least (s ∪ t) a ↔ is_least s a ∧ a ∈ lower_bounds t ∨ a ∈ lower_bounds s ∧ is_least t a
source
theorem is_greatest_union_iff {α : Type u} [preorder α] {s t : set α} {a : α} :
is_greatest (s ∪ t) a ↔ is_greatest s a ∧ a ∈ upper_bounds t ∨ a ∈ upper_bounds s ∧ is_greatest t a
source
theorem bdd_above.inter_of_left {α : Type u} [preorder α] {s t : set α} (h : bdd_above s) :
bdd_above (s ∩ t)

If s is bounded, then so is s ∩ t

source
theorem bdd_above.inter_of_right {α : Type u} [preorder α] {s t : set α} (h : bdd_above t) :
bdd_above (s ∩ t)

If t is bounded, then so is s ∩ t

source
theorem bdd_below.inter_of_left {α : Type u} [preorder α] {s t : set α} (h : bdd_below s) :
bdd_below (s ∩ t)

If s is bounded, then so is s ∩ t

source
theorem bdd_below.inter_of_right {α : Type u} [preorder α] {s t : set α} (h : bdd_below t) :
bdd_below (s ∩ t)

If t is bounded, then so is s ∩ t

source
theorem bdd_above.union {α : Type u} [preorder α] [is_directed α has_le.le] {s t : set α} :
bdd_above s → bdd_above t → bdd_above (s ∪ t)

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

source
theorem bdd_above_union {α : Type u} [preorder α] [is_directed α has_le.le] {s t : set α} :
bdd_above (s ∪ t) ↔ bdd_above s ∧ bdd_above t

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

source
theorem bdd_below.union {α : Type u} [preorder α] [is_directed α ge] {s t : set α} :
bdd_below s → bdd_below t → bdd_below (s ∪ t)

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

source
theorem bdd_below_union {α : Type u} [preorder α] [is_directed α ge] {s t : set α} :
bdd_below (s ∪ t) ↔ bdd_below s ∧ bdd_below t

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

source
theorem is_lub.union {γ : Type w} [semilattice_sup γ] {a b : γ} {s t : set γ} (hs : is_lub s a) (ht : is_lub t b) :
is_lub (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.

source
theorem is_glb.union {γ : Type w} [semilattice_inf γ] {a₁ a₂ : γ} {s t : set γ} (hs : is_glb s a₁) (ht : is_glb t a₂) :
is_glb (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.

source
theorem is_least.union {γ : Type w} [linear_order γ] {a b : γ} {s t : set γ} (ha : is_least s a) (hb : is_least t b) :
is_least (s ∪ t) (linear_order.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.

source
theorem is_greatest.union {γ : Type w} [linear_order γ] {a b : γ} {s t : set γ} (ha : is_greatest s a) (hb : is_greatest t b) :
is_greatest (s ∪ t) (linear_order.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.

source
theorem is_lub.inter_Ici_of_mem {γ : Type w} [linear_order γ] {s : set γ} {a b : γ} (ha : is_lub s a) (hb : b ∈ s) :
is_lub (s ∩ set.Ici b) a
source
theorem is_glb.inter_Iic_of_mem {γ : Type w} [linear_order γ] {s : set γ} {a b : γ} (ha : is_glb s a) (hb : b ∈ s) :
is_glb (s ∩ set.Iic b) a
source
theorem bdd_above_iff_exists_ge {γ : Type w} [semilattice_sup γ] {s : set γ} (x₀ : γ) :
bdd_above s ↔ ∃ (x : γ), x₀ ≤ x ∧ ∀ (y : γ), y ∈ s → y ≤ x
source
theorem bdd_below_iff_exists_le {γ : Type w} [semilattice_inf γ] {s : set γ} (x₀ : γ) :
bdd_below s ↔ ∃ (x : γ), x ≤ x₀ ∧ ∀ (y : γ), y ∈ s → x ≤ y
source
theorem bdd_above.exists_ge {γ : Type w} [semilattice_sup γ] {s : set γ} (hs : bdd_above s) (x₀ : γ) :
∃ (x : γ), x₀ ≤ x ∧ ∀ (y : γ), y ∈ s → y ≤ x
source
theorem bdd_below.exists_le {γ : Type w} [semilattice_inf γ] {s : set γ} (hs : bdd_below s) (x₀ : γ) :
∃ (x : γ), x ≤ x₀ ∧ ∀ (y : γ), y ∈ s → x ≤ y

Specific sets #

Unbounded intervals #

source
theorem is_least_Ici {α : Type u} [preorder α] {a : α} :
is_least (set.Ici a) a
source
theorem is_greatest_Iic {α : Type u} [preorder α] {a : α} :
is_greatest (set.Iic a) a
source
theorem is_lub_Iic {α : Type u} [preorder α] {a : α} :
is_lub (set.Iic a) a
source
theorem is_glb_Ici {α : Type u} [preorder α] {a : α} :
is_glb (set.Ici a) a
source
theorem upper_bounds_Iic {α : Type u} [preorder α] {a : α} :
upper_bounds (set.Iic a) = set.Ici a
source
theorem lower_bounds_Ici {α : Type u} [preorder α] {a : α} :
lower_bounds (set.Ici a) = set.Iic a
source
theorem bdd_above_Iic {α : Type u} [preorder α] {a : α} :
bdd_above (set.Iic a)
source
theorem bdd_below_Ici {α : Type u} [preorder α] {a : α} :
bdd_below (set.Ici a)
source
theorem bdd_above_Iio {α : Type u} [preorder α] {a : α} :
bdd_above (set.Iio a)
source
theorem bdd_below_Ioi {α : Type u} [preorder α] {a : α} :
bdd_below (set.Ioi a)
source
theorem lub_Iio_le {α : Type u} [preorder α] {b : α} (a : α) (hb : is_lub (set.Iio a) b) :
b ≤ a
source
theorem le_glb_Ioi {α : Type u} [preorder α] {b : α} (a : α) (hb : is_glb (set.Ioi a) b) :
a ≤ b
source
theorem lub_Iio_eq_self_or_Iio_eq_Iic {γ : Type w} [partial_order γ] {j : γ} (i : γ) (hj : is_lub (set.Iio i) j) :
j = i ∨ set.Iio i = set.Iic j
source
theorem glb_Ioi_eq_self_or_Ioi_eq_Ici {γ : Type w} [partial_order γ] {j : γ} (i : γ) (hj : is_glb (set.Ioi i) j) :
j = i ∨ set.Ioi i = set.Ici j
source
theorem exists_lub_Iio {γ : Type w} [linear_order γ] (i : γ) :
∃ (j : γ), is_lub (set.Iio i) j
source
theorem exists_glb_Ioi {γ : Type w} [linear_order γ] (i : γ) :
∃ (j : γ), is_glb (set.Ioi i) j
source
theorem is_lub_Iio {γ : Type w} [linear_order γ] [densely_ordered γ] {a : γ} :
is_lub (set.Iio a) a
source
theorem is_glb_Ioi {γ : Type w} [linear_order γ] [densely_ordered γ] {a : γ} :
is_glb (set.Ioi a) a
source
theorem upper_bounds_Iio {γ : Type w} [linear_order γ] [densely_ordered γ] {a : γ} :
upper_bounds (set.Iio a) = set.Ici a
source
theorem lower_bounds_Ioi {γ : Type w} [linear_order γ] [densely_ordered γ] {a : γ} :
lower_bounds (set.Ioi a) = set.Iic a

Singleton #

source
theorem is_greatest_singleton {α : Type u} [preorder α] {a : α} :
is_greatest {a} a
source
theorem is_least_singleton {α : Type u} [preorder α] {a : α} :
is_least {a} a
source
theorem is_lub_singleton {α : Type u} [preorder α] {a : α} :
is_lub {a} a
source
theorem is_glb_singleton {α : Type u} [preorder α] {a : α} :
is_glb {a} a
source
theorem bdd_above_singleton {α : Type u} [preorder α] {a : α} :
bdd_above {a}
source
theorem bdd_below_singleton {α : Type u} [preorder α] {a : α} :
bdd_below {a}
source
@[simp]
theorem upper_bounds_singleton {α : Type u} [preorder α] {a : α} :
upper_bounds {a} = set.Ici a
source
@[simp]
theorem lower_bounds_singleton {α : Type u} [preorder α] {a : α} :
lower_bounds {a} = set.Iic a

Bounded intervals #

source
theorem bdd_above_Icc {α : Type u} [preorder α] {a b : α} :
bdd_above (set.Icc a b)
source
theorem bdd_below_Icc {α : Type u} [preorder α] {a b : α} :
bdd_below (set.Icc a b)
source
theorem bdd_above_Ico {α : Type u} [preorder α] {a b : α} :
bdd_above (set.Ico a b)
source
theorem bdd_below_Ico {α : Type u} [preorder α] {a b : α} :
bdd_below (set.Ico a b)
source
theorem bdd_above_Ioc {α : Type u} [preorder α] {a b : α} :
bdd_above (set.Ioc a b)
source
theorem bdd_below_Ioc {α : Type u} [preorder α] {a b : α} :
bdd_below (set.Ioc a b)
source
theorem bdd_above_Ioo {α : Type u} [preorder α] {a b : α} :
bdd_above (set.Ioo a b)
source
theorem bdd_below_Ioo {α : Type u} [preorder α] {a b : α} :
bdd_below (set.Ioo a b)
source
theorem is_greatest_Icc {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :
is_greatest (set.Icc a b) b
source
theorem is_lub_Icc {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :
is_lub (set.Icc a b) b
source
theorem upper_bounds_Icc {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :
upper_bounds (set.Icc a b) = set.Ici b
source
theorem is_least_Icc {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :
is_least (set.Icc a b) a
source
theorem is_glb_Icc {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :
is_glb (set.Icc a b) a
source
theorem lower_bounds_Icc {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :
lower_bounds (set.Icc a b) = set.Iic a
source
theorem is_greatest_Ioc {α : Type u} [preorder α] {a b : α} (h : a < b) :
is_greatest (set.Ioc a b) b
source
theorem is_lub_Ioc {α : Type u} [preorder α] {a b : α} (h : a < b) :
is_lub (set.Ioc a b) b
source
theorem upper_bounds_Ioc {α : Type u} [preorder α] {a b : α} (h : a < b) :
upper_bounds (set.Ioc a b) = set.Ici b
source
theorem is_least_Ico {α : Type u} [preorder α] {a b : α} (h : a < b) :
is_least (set.Ico a b) a
source
theorem is_glb_Ico {α : Type u} [preorder α] {a b : α} (h : a < b) :
is_glb (set.Ico a b) a
source
theorem lower_bounds_Ico {α : Type u} [preorder α] {a b : α} (h : a < b) :
lower_bounds (set.Ico a b) = set.Iic a
source
theorem is_glb_Ioo {γ : Type w} [semilattice_sup γ] [densely_ordered γ] {a b : γ} (h : a < b) :
is_glb (set.Ioo a b) a
source
theorem lower_bounds_Ioo {γ : Type w} [semilattice_sup γ] [densely_ordered γ] {a b : γ} (hab : a < b) :
lower_bounds (set.Ioo a b) = set.Iic a
source
theorem is_glb_Ioc {γ : Type w} [semilattice_sup γ] [densely_ordered γ] {a b : γ} (hab : a < b) :
is_glb (set.Ioc a b) a
source
theorem lower_bound_Ioc {γ : Type w} [semilattice_sup γ] [densely_ordered γ] {a b : γ} (hab : a < b) :
lower_bounds (set.Ioc a b) = set.Iic a
source
theorem is_lub_Ioo {γ : Type w} [semilattice_inf γ] [densely_ordered γ] {a b : γ} (hab : a < b) :
is_lub (set.Ioo a b) b
source
theorem upper_bounds_Ioo {γ : Type w} [semilattice_inf γ] [densely_ordered γ] {a b : γ} (hab : a < b) :
upper_bounds (set.Ioo a b) = set.Ici b
source
theorem is_lub_Ico {γ : Type w} [semilattice_inf γ] [densely_ordered γ] {a b : γ} (hab : a < b) :
is_lub (set.Ico a b) b
source
theorem upper_bounds_Ico {γ : Type w} [semilattice_inf γ] [densely_ordered γ] {a b : γ} (hab : a < b) :
upper_bounds (set.Ico a b) = set.Ici b
source
theorem bdd_below_iff_subset_Ici {α : Type u} [preorder α] {s : set α} :
bdd_below s ↔ ∃ (a : α), s ⊆ set.Ici a
source
theorem bdd_above_iff_subset_Iic {α : Type u} [preorder α] {s : set α} :
bdd_above s ↔ ∃ (a : α), s ⊆ set.Iic a
source
theorem bdd_below_bdd_above_iff_subset_Icc {α : Type u} [preorder α] {s : set α} :
bdd_below s ∧ bdd_above s ↔ ∃ (a b : α), s ⊆ set.Icc a b

Univ #

source
@[simp]
theorem is_greatest_univ_iff {α : Type u} [preorder α] {a : α} :
is_greatest set.univ a ↔ is_top a
source
theorem is_greatest_univ {α : Type u} [preorder α] [order_top α] :
is_greatest set.univ ⊤
source
@[simp]
theorem order_top.upper_bounds_univ {γ : Type w} [partial_order γ] [order_top γ] :
upper_bounds set.univ = {⊤}
source
theorem is_lub_univ {α : Type u} [preorder α] [order_top α] :
is_lub set.univ ⊤
source
@[simp]
theorem order_bot.lower_bounds_univ {γ : Type w} [partial_order γ] [order_bot γ] :
lower_bounds set.univ = {⊥}
source
@[simp]
theorem is_least_univ_iff {α : Type u} [preorder α] {a : α} :
is_least set.univ a ↔ is_bot a
source
theorem is_least_univ {α : Type u} [preorder α] [order_bot α] :
is_least set.univ ⊥
source
theorem is_glb_univ {α : Type u} [preorder α] [order_bot α] :
is_glb set.univ ⊥
source
@[simp]
theorem no_max_order.upper_bounds_univ {α : Type u} [preorder α] [no_max_order α] :
upper_bounds set.univ = ∅
source
@[simp]
theorem no_min_order.lower_bounds_univ {α : Type u} [preorder α] [no_min_order α] :
lower_bounds set.univ = ∅
source
@[simp]
theorem not_bdd_above_univ {α : Type u} [preorder α] [no_max_order α] :
¬bdd_above set.univ
source
@[simp]
theorem not_bdd_below_univ {α : Type u} [preorder α] [no_min_order α] :
¬bdd_below set.univ

Empty set #

source
@[simp]
theorem upper_bounds_empty {α : Type u} [preorder α] :
upper_bounds ∅ = set.univ
source
@[simp]
theorem lower_bounds_empty {α : Type u} [preorder α] :
lower_bounds ∅ = set.univ
source
@[simp]
theorem bdd_above_empty {α : Type u} [preorder α] [nonempty α] :
bdd_above ∅
source
@[simp]
theorem bdd_below_empty {α : Type u} [preorder α] [nonempty α] :
bdd_below ∅
source
@[simp]
theorem is_glb_empty_iff {α : Type u} [preorder α] {a : α} :
is_glb ∅ a ↔ is_top a
source
@[simp]
theorem is_lub_empty_iff {α : Type u} [preorder α] {a : α} :
is_lub ∅ a ↔ is_bot a
source
theorem is_glb_empty {α : Type u} [preorder α] [order_top α] :
is_glb ∅ ⊤
source
theorem is_lub_empty {α : Type u} [preorder α] [order_bot α] :
is_lub ∅ ⊥
source
theorem is_lub.nonempty {α : Type u} [preorder α] {s : set α} {a : α} [no_min_order α] (hs : is_lub s a) :
s.nonempty
source
theorem is_glb.nonempty {α : Type u} [preorder α] {s : set α} {a : α} [no_max_order α] (hs : is_glb s a) :
s.nonempty
source
theorem nonempty_of_not_bdd_above {α : Type u} [preorder α] {s : set α} [ha : nonempty α] (h : ¬bdd_above s) :
s.nonempty
source
theorem nonempty_of_not_bdd_below {α : Type u} [preorder α] {s : set α} [ha : nonempty α] (h : ¬bdd_below s) :
s.nonempty

insert #

source
@[simp]
theorem bdd_above_insert {α : Type u} [preorder α] [is_directed α has_le.le] {s : set α} {a : α} :
bdd_above (has_insert.insert a s) ↔ bdd_above s

Adding a point to a set preserves its boundedness above.

source
@[protected]
theorem bdd_above.insert {α : Type u} [preorder α] [is_directed α has_le.le] {s : set α} (a : α) :
bdd_above s → bdd_above (has_insert.insert a s)
source
@[simp]
theorem bdd_below_insert {α : Type u} [preorder α] [is_directed α ge] {s : set α} {a : α} :
bdd_below (has_insert.insert a s) ↔ bdd_below s

Adding a point to a set preserves its boundedness below.

source
theorem bdd_below.insert {α : Type u} [preorder α] [is_directed α ge] {s : set α} (a : α) :
bdd_below s → bdd_below (has_insert.insert a s)
source
theorem is_lub.insert {γ : Type w} [semilattice_sup γ] (a : γ) {b : γ} {s : set γ} (hs : is_lub s b) :
is_lub (has_insert.insert a s) (a ⊔ b)
source
theorem is_glb.insert {γ : Type w} [semilattice_inf γ] (a : γ) {b : γ} {s : set γ} (hs : is_glb s b) :
is_glb (has_insert.insert a s) (a ⊓ b)
source
theorem is_greatest.insert {γ : Type w} [linear_order γ] (a : γ) {b : γ} {s : set γ} (hs : is_greatest s b) :
is_greatest (has_insert.insert a s) (linear_order.max a b)
source
theorem is_least.insert {γ : Type w} [linear_order γ] (a : γ) {b : γ} {s : set γ} (hs : is_least s b) :
is_least (has_insert.insert a s) (linear_order.min a b)
source
@[simp]
theorem upper_bounds_insert {α : Type u} [preorder α] (a : α) (s : set α) :
upper_bounds (has_insert.insert a s) = set.Ici a ∩ upper_bounds s
source
@[simp]
theorem lower_bounds_insert {α : Type u} [preorder α] (a : α) (s : set α) :
lower_bounds (has_insert.insert a s) = set.Iic a ∩ lower_bounds s
source
@[protected, simp]
theorem order_top.bdd_above {α : Type u} [preorder α] [order_top α] (s : set α) :
bdd_above s

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

source
@[protected, simp]
theorem order_bot.bdd_below {α : Type u} [preorder α] [order_bot α] (s : set α) :
bdd_below s

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

Pair #

source
theorem is_lub_pair {γ : Type w} [semilattice_sup γ] {a b : γ} :
is_lub {a, b} (a ⊔ b)
source
theorem is_glb_pair {γ : Type w} [semilattice_inf γ] {a b : γ} :
is_glb {a, b} (a ⊓ b)
source
theorem is_least_pair {γ : Type w} [linear_order γ] {a b : γ} :
is_least {a, b} (linear_order.min a b)
source
theorem is_greatest_pair {γ : Type w} [linear_order γ] {a b : γ} :
is_greatest {a, b} (linear_order.max a b)

Lower/upper bounds #

source
@[simp]
theorem is_lub_lower_bounds {α : Type u} [preorder α] {s : set α} {a : α} :
is_lub (lower_bounds s) a ↔ is_glb s a
source
@[simp]
theorem is_glb_upper_bounds {α : Type u} [preorder α] {s : set α} {a : α} :
is_glb (upper_bounds s) a ↔ is_lub s a

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

source
theorem lower_bounds_le_upper_bounds {α : Type u} [preorder α] {s : set α} {a b : α} (ha : a ∈ lower_bounds s) (hb : b ∈ upper_bounds s) :
s.nonempty → a ≤ b
source
theorem is_glb_le_is_lub {α : Type u} [preorder α] {s : set α} {a b : α} (ha : is_glb s a) (hb : is_lub s b) (hs : s.nonempty) :
a ≤ b
source
theorem is_lub_lt_iff {α : Type u} [preorder α] {s : set α} {a b : α} (ha : is_lub s a) :
a < b ↔ ∃ (c : α) (H : c ∈ upper_bounds s), c < b
source
theorem lt_is_glb_iff {α : Type u} [preorder α] {s : set α} {a b : α} (ha : is_glb s a) :
b < a ↔ ∃ (c : α) (H : c ∈ lower_bounds s), b < c
source
theorem le_of_is_lub_le_is_glb {α : Type u} [preorder α] {s : set α} {a b x y : α} (ha : is_glb s a) (hb : is_lub s b) (hab : b ≤ a) (hx : x ∈ s) (hy : y ∈ s) :
x ≤ y
source
theorem is_least.unique {α : Type u} [partial_order α] {s : set α} {a b : α} (Ha : is_least s a) (Hb : is_least s b) :
a = b
source
theorem is_least.is_least_iff_eq {α : Type u} [partial_order α] {s : set α} {a b : α} (Ha : is_least s a) :
is_least s b ↔ a = b
source
theorem is_greatest.unique {α : Type u} [partial_order α] {s : set α} {a b : α} (Ha : is_greatest s a) (Hb : is_greatest s b) :
a = b
source
theorem is_greatest.is_greatest_iff_eq {α : Type u} [partial_order α] {s : set α} {a b : α} (Ha : is_greatest s a) :
is_greatest s b ↔ a = b
source
theorem is_lub.unique {α : Type u} [partial_order α] {s : set α} {a b : α} (Ha : is_lub s a) (Hb : is_lub s b) :
a = b
source
theorem is_glb.unique {α : Type u} [partial_order α] {s : set α} {a b : α} (Ha : is_glb s a) (Hb : is_glb s b) :
a = b
source
theorem set.subsingleton_of_is_lub_le_is_glb {α : Type u} [partial_order α] {s : set α} {a b : α} (Ha : is_glb s a) (Hb : is_lub s b) (hab : b ≤ a) :
s.subsingleton
source
theorem is_glb_lt_is_lub_of_ne {α : Type u} [partial_order α] {s : set α} {a b : α} (Ha : is_glb s a) (Hb : is_lub s b) {x y : α} (Hx : x ∈ s) (Hy : y ∈ s) (Hxy : x ≠ y) :
a < b
source
theorem lt_is_lub_iff {α : Type u} [linear_order α] {s : set α} {a b : α} (h : is_lub s a) :
b < a ↔ ∃ (c : α) (H : c ∈ s), b < c
source
theorem is_glb_lt_iff {α : Type u} [linear_order α] {s : set α} {a b : α} (h : is_glb s a) :
a < b ↔ ∃ (c : α) (H : c ∈ s), c < b
source
theorem is_lub.exists_between {α : Type u} [linear_order α] {s : set α} {a b : α} (h : is_lub s a) (hb : b < a) :
∃ (c : α) (H : c ∈ s), b < c ∧ c ≤ a
source
theorem is_lub.exists_between' {α : Type u} [linear_order α] {s : set α} {a b : α} (h : is_lub s a) (h' : a ∉ s) (hb : b < a) :
∃ (c : α) (H : c ∈ s), b < c ∧ c < a
source
theorem is_glb.exists_between {α : Type u} [linear_order α] {s : set α} {a b : α} (h : is_glb s a) (hb : a < b) :
∃ (c : α) (H : c ∈ s), a ≤ c ∧ c < b
source
theorem is_glb.exists_between' {α : Type u} [linear_order α] {s : set α} {a b : α} (h : is_glb s a) (h' : a ∉ s) (hb : a < b) :
∃ (c : α) (H : c ∈ s), a < c ∧ c < b

Images of upper/lower bounds under monotone functions #

source
theorem monotone_on.mem_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : monotone_on f t) {a : α} (Hst : s ⊆ t) (Has : a ∈ upper_bounds s) (Hat : a ∈ t) :
f a ∈ upper_bounds (f '' s)
source
theorem monotone_on.mem_upper_bounds_image_self {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : monotone_on f t) {a : α} :
a ∈ upper_bounds t → a ∈ t → f a ∈ upper_bounds (f '' t)
source
theorem monotone_on.mem_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : monotone_on f t) {a : α} (Hst : s ⊆ t) (Has : a ∈ lower_bounds s) (Hat : a ∈ t) :
f a ∈ lower_bounds (f '' s)
source
theorem monotone_on.mem_lower_bounds_image_self {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : monotone_on f t) {a : α} :
a ∈ lower_bounds t → a ∈ t → f a ∈ lower_bounds (f '' t)
source
theorem monotone_on.image_upper_bounds_subset_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : monotone_on f t) (Hst : s ⊆ t) :
f '' (upper_bounds s ∩ t) ⊆ upper_bounds (f '' s)
source
theorem monotone_on.image_lower_bounds_subset_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : monotone_on f t) (Hst : s ⊆ t) :
f '' (lower_bounds s ∩ t) ⊆ lower_bounds (f '' s)
source
theorem monotone_on.map_bdd_above {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : monotone_on f t) (Hst : s ⊆ t) :
(upper_bounds s ∩ t).nonempty → bdd_above (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.

source
theorem monotone_on.map_bdd_below {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : monotone_on f t) (Hst : s ⊆ t) :
(lower_bounds s ∩ t).nonempty → bdd_below (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.

source
theorem monotone_on.map_is_least {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : monotone_on f t) {a : α} (Ha : is_least t a) :
is_least (f '' t) (f a)

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

source
theorem monotone_on.map_is_greatest {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : monotone_on f t) {a : α} (Ha : is_greatest t a) :
is_greatest (f '' t) (f a)

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

source
theorem antitone_on.mem_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : antitone_on f t) {a : α} (Hst : s ⊆ t) (Has : a ∈ lower_bounds s) :
a ∈ t → f a ∈ upper_bounds (f '' s)
source
theorem antitone_on.mem_upper_bounds_image_self {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : antitone_on f t) {a : α} :
a ∈ lower_bounds t → a ∈ t → f a ∈ upper_bounds (f '' t)
source
theorem antitone_on.mem_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : antitone_on f t) {a : α} (Hst : s ⊆ t) :
a ∈ upper_bounds s → a ∈ t → f a ∈ lower_bounds (f '' s)
source
theorem antitone_on.mem_lower_bounds_image_self {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : antitone_on f t) {a : α} :
a ∈ upper_bounds t → a ∈ t → f a ∈ lower_bounds (f '' t)
source
theorem antitone_on.image_lower_bounds_subset_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : antitone_on f t) (Hst : s ⊆ t) :
f '' (lower_bounds s ∩ t) ⊆ upper_bounds (f '' s)
source
theorem antitone_on.image_upper_bounds_subset_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : antitone_on f t) (Hst : s ⊆ t) :
f '' (upper_bounds s ∩ t) ⊆ lower_bounds (f '' s)
source
theorem antitone_on.map_bdd_above {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : antitone_on f t) (Hst : s ⊆ t) :
(upper_bounds s ∩ t).nonempty → bdd_below (f '' s)

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

source
theorem antitone_on.map_bdd_below {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : antitone_on f t) (Hst : s ⊆ t) :
(lower_bounds s ∩ t).nonempty → bdd_above (f '' s)

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

source
theorem antitone_on.map_is_greatest {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : antitone_on f t) {a : α} :
is_greatest t a → is_least (f '' t) (f a)

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

source
theorem antitone_on.map_is_least {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : antitone_on f t) {a : α} :
is_least t a → is_greatest (f '' t) (f a)

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

source
theorem monotone.mem_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} (Ha : a ∈ upper_bounds s) :
f a ∈ upper_bounds (f '' s)
source
theorem monotone.mem_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} (Ha : a ∈ lower_bounds s) :
f a ∈ lower_bounds (f '' s)
source
theorem monotone.image_upper_bounds_subset_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {s : set α} :
f '' upper_bounds s ⊆ upper_bounds (f '' s)
source
theorem monotone.image_lower_bounds_subset_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {s : set α} :
f '' lower_bounds s ⊆ lower_bounds (f '' s)
source
theorem monotone.map_bdd_above {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {s : set α} :
bdd_above s → bdd_above (f '' s)

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

source
theorem monotone.map_bdd_below {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {s : set α} :
bdd_below s → bdd_below (f '' s)

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

source
theorem monotone.map_is_least {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} (Ha : is_least s a) :
is_least (f '' s) (f a)

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

source
theorem monotone.map_is_greatest {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} (Ha : is_greatest s a) :
is_greatest (f '' s) (f a)

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

source
theorem antitone.mem_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {a : α} {s : set α} :
a ∈ lower_bounds s → f a ∈ upper_bounds (f '' s)
source
theorem antitone.mem_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {a : α} {s : set α} :
a ∈ upper_bounds s → f a ∈ lower_bounds (f '' s)
source
theorem antitone.image_lower_bounds_subset_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {s : set α} :
f '' lower_bounds s ⊆ upper_bounds (f '' s)
source
theorem antitone.image_upper_bounds_subset_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {s : set α} :
f '' upper_bounds s ⊆ lower_bounds (f '' s)
source
theorem antitone.map_bdd_above {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {s : set α} :
bdd_above s → bdd_below (f '' s)

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

source
theorem antitone.map_bdd_below {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {s : set α} :
bdd_below s → bdd_above (f '' s)

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

source
theorem antitone.map_is_greatest {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {a : α} {s : set α} :
is_greatest s a → is_least (f '' s) (f a)

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

source
theorem antitone.map_is_least {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {a : α} {s : set α} :
is_least s a → is_greatest (f '' s) (f a)

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

source
theorem mem_upper_bounds_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 ∈ upper_bounds s) (hb : b ∈ upper_bounds t) :
f a b ∈ upper_bounds (set.image2 f s t)
source
theorem mem_lower_bounds_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 ∈ lower_bounds s) (hb : b ∈ lower_bounds t) :
f a b ∈ lower_bounds (set.image2 f s t)
source
theorem image2_upper_bounds_upper_bounds_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 (upper_bounds s) (upper_bounds t) ⊆ upper_bounds (set.image2 f s t)
source
theorem image2_lower_bounds_lower_bounds_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 (lower_bounds s) (lower_bounds t) ⊆ lower_bounds (set.image2 f s t)
source
theorem bdd_above.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)) :
bdd_above s → bdd_above t → bdd_above (set.image2 f s t)

See also monotone.map_bdd_above.

source
theorem bdd_below.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)) :
bdd_below s → bdd_below t → bdd_below (set.image2 f s t)

See also monotone.map_bdd_below.

source
theorem is_greatest.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 : is_greatest s a) (hb : is_greatest t b) :
is_greatest (set.image2 f s t) (f a b)
source
theorem is_least.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 : is_least s a) (hb : is_least t b) :
is_least (set.image2 f s t) (f a b)
source
theorem mem_upper_bounds_image2_of_mem_upper_bounds_of_mem_lower_bounds {α : 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 ∈ upper_bounds s) (hb : b ∈ lower_bounds t) :
f a b ∈ upper_bounds (set.image2 f s t)
source
theorem mem_lower_bounds_image2_of_mem_lower_bounds_of_mem_upper_bounds {α : 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 ∈ lower_bounds s) (hb : b ∈ upper_bounds t) :
f a b ∈ lower_bounds (set.image2 f s t)
source
theorem image2_upper_bounds_lower_bounds_subset_upper_bounds_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 (upper_bounds s) (lower_bounds t) ⊆ upper_bounds (set.image2 f s t)
source
theorem image2_lower_bounds_upper_bounds_subset_lower_bounds_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 (lower_bounds s) (upper_bounds t) ⊆ lower_bounds (set.image2 f s t)
source
theorem bdd_above.bdd_above_image2_of_bdd_below {α : 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)) :
bdd_above s → bdd_below t → bdd_above (set.image2 f s t)
source
theorem bdd_below.bdd_below_image2_of_bdd_above {α : 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)) :
bdd_below s → bdd_above t → bdd_below (set.image2 f s t)
source
theorem is_greatest.is_greatest_image2_of_is_least {α : 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 : is_greatest s a) (hb : is_least t b) :
is_greatest (set.image2 f s t) (f a b)
source
theorem is_least.is_least_image2_of_is_greatest {α : 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 : is_least s a) (hb : is_greatest t b) :
is_least (set.image2 f s t) (f a b)
source
theorem mem_upper_bounds_image2_of_mem_lower_bounds {α : 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 ∈ lower_bounds s) (hb : b ∈ lower_bounds t) :
f a b ∈ upper_bounds (set.image2 f s t)
source
theorem mem_lower_bounds_image2_of_mem_upper_bounds {α : 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 ∈ upper_bounds s) (hb : b ∈ upper_bounds t) :
f a b ∈ lower_bounds (set.image2 f s t)
source
theorem image2_upper_bounds_upper_bounds_subset_upper_bounds_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 (lower_bounds s) (lower_bounds t) ⊆ upper_bounds (set.image2 f s t)
source
theorem image2_lower_bounds_lower_bounds_subset_lower_bounds_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 (upper_bounds s) (upper_bounds t) ⊆ lower_bounds (set.image2 f s t)
source
theorem bdd_below.image2_bdd_above {α : 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)) :
bdd_below s → bdd_below t → bdd_above (set.image2 f s t)
source
theorem bdd_above.image2_bdd_below {α : 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)) :
bdd_above s → bdd_above t → bdd_below (set.image2 f s t)
source
theorem is_least.is_greatest_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 : is_least s a) (hb : is_least t b) :
is_greatest (set.image2 f s t) (f a b)
source
theorem is_greatest.is_least_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 : is_greatest s a) (hb : is_greatest t b) :
is_least (set.image2 f s t) (f a b)
source
theorem mem_upper_bounds_image2_of_mem_upper_bounds_of_mem_upper_bounds {α : 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 ∈ lower_bounds s) (hb : b ∈ upper_bounds t) :
f a b ∈ upper_bounds (set.image2 f s t)
source
theorem mem_lower_bounds_image2_of_mem_lower_bounds_of_mem_lower_bounds {α : 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 ∈ upper_bounds s) (hb : b ∈ lower_bounds t) :
f a b ∈ lower_bounds (set.image2 f s t)
source
theorem image2_lower_bounds_upper_bounds_subset_upper_bounds_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 (lower_bounds s) (upper_bounds t) ⊆ upper_bounds (set.image2 f s t)
source
theorem image2_upper_bounds_lower_bounds_subset_lower_bounds_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 (upper_bounds s) (lower_bounds t) ⊆ lower_bounds (set.image2 f s t)
source
theorem bdd_below.bdd_above_image2_of_bdd_above {α : 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)) :
bdd_below s → bdd_above t → bdd_above (set.image2 f s t)
source
theorem bdd_above.bdd_below_image2_of_bdd_above {α : 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)) :
bdd_above s → bdd_below t → bdd_below (set.image2 f s t)
source
theorem is_least.is_greatest_image2_of_is_greatest {α : 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 : is_least s a) (hb : is_greatest t b) :
is_greatest (set.image2 f s t) (f a b)
source
theorem is_greatest.is_least_image2_of_is_least {α : 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 : is_greatest s a) (hb : is_least t b) :
is_least (set.image2 f s t) (f a b)
source
theorem is_glb.of_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) {s : set α} {x : α} (hx : is_glb (f '' s) (f x)) :
is_glb s x
source
theorem is_lub.of_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) {s : set α} {x : α} (hx : is_lub (f '' s) (f x)) :
is_lub s x
source
theorem is_lub_pi {α : Type u} {π : α → Type u_1} [Π (a : α), preorder (π a)] {s : set (Π (a : α), π a)} {f : Π (a : α), π a} :
is_lub s f ↔ ∀ (a : α), is_lub (function.eval a '' s) (f a)
source
theorem is_glb_pi {α : Type u} {π : α → Type u_1} [Π (a : α), preorder (π a)] {s : set (Π (a : α), π a)} {f : Π (a : α), π a} :
is_glb s f ↔ ∀ (a : α), is_glb (function.eval a '' s) (f a)
source
theorem is_lub_prod {α : Type u} {β : Type v} [preorder α] [preorder β] {s : set (α × β)} (p : α × β) :
is_lub s p ↔ is_lub (prod.fst '' s) p.fst ∧ is_lub (prod.snd '' s) p.snd
source
theorem is_glb_prod {α : Type u} {β : Type v} [preorder α] [preorder β] {s : set (α × β)} (p : α × β) :
is_glb s p ↔ is_glb (prod.fst '' s) p.fst ∧ is_glb (prod.snd '' s) p.snd
source
def scott_continuous {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α → β) :
Prop

A function between preorders is said to be Scott continuous if it preserves is_lub 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 → directed_on (≥) d → ∀ ⦃a⦄, is_glb d a → is_glb (f '' d) (f a)

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

Equations
source
@[protected]
theorem scott_continuous.monotone {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (h : scott_continuous f) :
monotone f