Documentation

def upperBounds {α : Type u} [inst : 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} [inst : 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} [inst : Preorder α] (s : Set α) :

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

Equations

BddAbove s = Set.Nonempty (upperBounds s)

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

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

Equations

BddBelow s = Set.Nonempty (lowerBounds s)

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

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} [inst : Preorder α] (s : Set α) (a : α) :

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} [inst : 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} [inst : 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} [inst : Preorder α] {s : Set α} {a : α} :

a ∈ upperBounds s ↔ ∀ (x : α), x ∈ s → x ≤ a

theorem mem_lowerBounds {α : Type u} [inst : Preorder α] {s : Set α} {a : α} :

a ∈ lowerBounds s ↔ ∀ (x : α), x ∈ s → a ≤ x

theorem bddAbove_def {α : Type u} [inst : Preorder α] {s : Set α} :

BddAbove s ↔ ∃ x, ∀ (y : α), y ∈ s → y ≤ x

theorem bddBelow_def {α : Type u} [inst : Preorder α] {s : Set α} :

BddBelow s ↔ ∃ x, ∀ (y : α), y ∈ s → x ≤ y

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

⊥ ∈ lowerBounds s

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

⊤ ∈ upperBounds s

@[simp]

theorem isLeast_bot_iff {α : Type u} [inst : Preorder α] {s : Set α} [inst : OrderBot α] :

IsLeast s ⊥ ↔ ⊥ ∈ s

@[simp]

theorem isGreatest_top_iff {α : Type u} [inst : Preorder α] {s : Set α} [inst : OrderTop α] :

IsGreatest s ⊤ ↔ ⊤ ∈ s

theorem not_bddAbove_iff' {α : Type u} [inst : 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∈ s such that x is not greater than or equal to y. This version only assumes Preorder structure and uses ¬(y ≤ x)¬(y ≤ x)≤ x). A version for linear orders is called not_bddAbove_iff.

theorem not_bddBelow_iff' {α : Type u} [inst : 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∈ s such that x is not less than or equal to y. This version only assumes Preorder structure and uses ¬(x ≤ y)¬(x ≤ y)≤ y). A version for linear orders is called not_bddBelow_iff.

theorem not_bddAbove_iff {α : Type u_1} [inst : 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∈ s that is greater than x. A version for preorders is called not_bddAbove_iff'.

theorem not_bddBelow_iff {α : Type u_1} [inst : 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∈ s that is less than x. A version for preorders is called not_bddBelow_iff'.

theorem BddAbove.dual {α : Type u} [inst : Preorder α] {s : Set α} (h : BddAbove s) :

BddBelow (↑OrderDual.ofDual ⁻¹' s)

theorem BddBelow.dual {α : Type u} [inst : Preorder α] {s : Set α} (h : BddBelow s) :

BddAbove (↑OrderDual.ofDual ⁻¹' s)

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

IsGreatest (↑OrderDual.ofDual ⁻¹' s) (↑OrderDual.toDual a)

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

IsLeast (↑OrderDual.ofDual ⁻¹' s) (↑OrderDual.toDual a)

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

IsGLB (↑OrderDual.ofDual ⁻¹' s) (↑OrderDual.toDual a)

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

IsLUB (↑OrderDual.ofDual ⁻¹' s) (↑OrderDual.toDual a)

def IsLeast.orderBot {α : Type u} [inst : 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)

def IsGreatest.orderTop {α : Type u} [inst : 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} [inst : Preorder α] ⦃s : Set α⦄ ⦃t : Set α⦄ (hst : s ⊆ t) :

upperBounds t ⊆ upperBounds s

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

lowerBounds t ⊆ lowerBounds s

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

a ∈ upperBounds s → b ∈ upperBounds s

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

b ∈ lowerBounds s → a ∈ lowerBounds s

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

a ∈ upperBounds t → b ∈ upperBounds s

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

b ∈ lowerBounds t → a ∈ lowerBounds s

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

BddAbove t → BddAbove s

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

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

BddBelow t → BddBelow s

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

theorem IsLUB.of_subset_of_superset {α : Type u} [inst : 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⊆ t ⊆ p⊆ p.

theorem IsGLB.of_subset_of_superset {α : Type u} [inst : 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⊆ t ⊆ p⊆ p.

theorem IsLeast.mono {α : Type u} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Preorder α] (s : Set α) :

s ⊆ lowerBounds (upperBounds s)

theorem subset_upperBounds_lowerBounds {α : Type u} [inst : Preorder α] (s : Set α) :

s ⊆ upperBounds (lowerBounds s)

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

BddAbove (lowerBounds s)

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

BddBelow (upperBounds s)

Conversions #

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

IsGLB s a

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

IsLUB s a

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

upperBounds s = Set.Ici a

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

lowerBounds s = Set.Iic a

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

lowerBounds s = Set.Iic a

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

upperBounds s = Set.Ici a

theorem IsGreatest.lt_iff {α : Type u} [inst : Preorder α] {s : Set α} {a : α} {b : α} (h : IsGreatest s a) :

a < b ↔ ∀ (x : α), x ∈ s → x < b

theorem IsLeast.lt_iff {α : Type u} [inst : Preorder α] {s : Set α} {a : α} {b : α} (h : IsLeast s a) :

b < a ↔ ∀ (x : α), x ∈ s → b < x

theorem isLUB_le_iff {α : Type u} [inst : Preorder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) :

a ≤ b ↔ b ∈ upperBounds s

theorem le_isGLB_iff {α : Type u} [inst : Preorder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) :

b ≤ a ↔ b ∈ lowerBounds s

theorem isLUB_iff_le_iff {α : Type u} [inst : Preorder α] {s : Set α} {a : α} :

IsLUB s a ↔ ∀ (b : α), a ≤ b ↔ b ∈ upperBounds s

theorem isGLB_iff_le_iff {α : Type u} [inst : Preorder α] {s : Set α} {a : α} :

IsGLB s a ↔ ∀ (b : α), b ≤ a ↔ b ∈ lowerBounds s

theorem IsLUB.bddAbove {α : Type u} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Preorder α] {s : Set α} {a : α} (h : IsLeast s a) :

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

Union and intersection #

@[simp]

theorem upperBounds_union {α : Type u} [inst : Preorder α] {s : Set α} {t : Set α} :

upperBounds (s ∪ t) = upperBounds s ∩ upperBounds t

@[simp]

theorem lowerBounds_union {α : Type u} [inst : Preorder α] {s : Set α} {t : Set α} :

lowerBounds (s ∪ t) = lowerBounds s ∩ lowerBounds t

theorem union_upperBounds_subset_upperBounds_inter {α : Type u} [inst : Preorder α] {s : Set α} {t : Set α} :

upperBounds s ∪ upperBounds t ⊆ upperBounds (s ∩ t)

theorem union_lowerBounds_subset_lowerBounds_inter {α : Type u} [inst : Preorder α] {s : Set α} {t : Set α} :

lowerBounds s ∪ lowerBounds t ⊆ lowerBounds (s ∩ t)

theorem isLeast_union_iff {α : Type u} [inst : 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} [inst : 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} [inst : Preorder α] {s : Set α} {t : Set α} (h : BddAbove s) :

BddAbove (s ∩ t)

If s is bounded, then so is s ∩ t∩ t

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

BddAbove (s ∩ t)

If t is bounded, then so is s ∩ t∩ t

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

BddBelow (s ∩ t)

If s is bounded, then so is s ∩ t∩ t

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

BddBelow (s ∩ t)

If t is bounded, then so is s ∩ t∩ t

theorem BddAbove.union {γ : Type w} [inst : SemilatticeSup γ] {s : Set γ} {t : Set γ} :

BddAbove s → BddAbove t → BddAbove (s ∪ t)

If s and t are bounded above sets in a semilattice_sup, then so is s ∪ t∪ t.

theorem bddAbove_union {γ : Type w} [inst : SemilatticeSup γ] {s : Set γ} {t : Set γ} :

BddAbove (s ∪ t) ↔ BddAbove s ∧ BddAbove t

The union of two sets is bounded above if and only if each of the sets is.

theorem BddBelow.union {γ : Type w} [inst : SemilatticeInf γ] {s : Set γ} {t : Set γ} :

BddBelow s → BddBelow t → BddBelow (s ∪ t)

theorem bddBelow_union {γ : Type w} [inst : SemilatticeInf γ] {s : Set γ} {t : Set γ} :

BddBelow (s ∪ t) ↔ BddBelow s ∧ BddBelow t

The union of two sets is bounded above if and only if each of the sets is.

theorem IsLUB.union {γ : Type w} [inst : 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⊔ b is the least upper bound of s ∪ t∪ t.

theorem IsGLB.union {γ : Type w} [inst : 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⊓ b is the greatest lower bound of s ∪ t∪ t.

theorem IsLeast.union {γ : Type w} [inst : 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∪ t.

theorem IsGreatest.union {γ : Type w} [inst : 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∪ t.

theorem IsLUB.inter_Ici_of_mem {γ : Type w} [inst : 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} [inst : 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} [inst : SemilatticeSup γ] {s : Set γ} (x₀ : γ) :

BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ (y : γ), y ∈ s → y ≤ x

theorem bddBelow_iff_exists_le {γ : Type w} [inst : SemilatticeInf γ] {s : Set γ} (x₀ : γ) :

BddBelow s ↔ ∃ x, x ≤ x₀ ∧ ∀ (y : γ), y ∈ s → x ≤ y

theorem BddAbove.exists_ge {γ : Type w} [inst : SemilatticeSup γ] {s : Set γ} (hs : BddAbove s) (x₀ : γ) :

∃ x, x₀ ≤ x ∧ ∀ (y : γ), y ∈ s → y ≤ x

theorem BddBelow.exists_le {γ : Type w} [inst : SemilatticeInf γ] {s : Set γ} (hs : BddBelow s) (x₀ : γ) :

∃ x, x ≤ x₀ ∧ ∀ (y : γ), y ∈ s → x ≤ y

Specific sets #

Unbounded intervals #

theorem isLeast_Ici {α : Type u} [inst : Preorder α] {a : α} :

IsLeast (Set.Ici a) a

theorem isGreatest_Iic {α : Type u} [inst : Preorder α] {a : α} :

IsGreatest (Set.Iic a) a

theorem isLUB_Iic {α : Type u} [inst : Preorder α] {a : α} :

IsLUB (Set.Iic a) a

theorem isGLB_Ici {α : Type u} [inst : Preorder α] {a : α} :

IsGLB (Set.Ici a) a

theorem upperBounds_Iic {α : Type u} [inst : Preorder α] {a : α} :

upperBounds (Set.Iic a) = Set.Ici a

theorem lowerBounds_Ici {α : Type u} [inst : Preorder α] {a : α} :

lowerBounds (Set.Ici a) = Set.Iic a

theorem bddAbove_Iic {α : Type u} [inst : Preorder α] {a : α} :

BddAbove (Set.Iic a)

theorem bddBelow_Ici {α : Type u} [inst : Preorder α] {a : α} :

BddBelow (Set.Ici a)

theorem bddAbove_Iio {α : Type u} [inst : Preorder α] {a : α} :

BddAbove (Set.Iio a)

theorem bddBelow_Ioi {α : Type u} [inst : Preorder α] {a : α} :

BddBelow (Set.Ioi a)

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

b ≤ a

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

a ≤ b

theorem lub_Iio_eq_self_or_Iio_eq_Iic {γ : Type w} [inst : 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} [inst : PartialOrder γ] {j : γ} (i : γ) (hj : IsGLB (Set.Ioi i) j) :

j = i ∨ Set.Ioi i = Set.Ici j

theorem exists_lub_Iio {γ : Type w} [inst : LinearOrder γ] (i : γ) :

∃ j, IsLUB (Set.Iio i) j

theorem exists_glb_Ioi {γ : Type w} [inst : LinearOrder γ] (i : γ) :

∃ j, IsGLB (Set.Ioi i) j

theorem isLUB_Iio {γ : Type w} [inst : LinearOrder γ] [inst : DenselyOrdered γ] {a : γ} :

IsLUB (Set.Iio a) a

theorem isGLB_Ioi {γ : Type w} [inst : LinearOrder γ] [inst : DenselyOrdered γ] {a : γ} :

IsGLB (Set.Ioi a) a

theorem upperBounds_Iio {γ : Type w} [inst : LinearOrder γ] [inst : DenselyOrdered γ] {a : γ} :

upperBounds (Set.Iio a) = Set.Ici a

theorem lowerBounds_Ioi {γ : Type w} [inst : LinearOrder γ] [inst : DenselyOrdered γ] {a : γ} :

lowerBounds (Set.Ioi a) = Set.Iic a

Singleton #

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

IsGreatest {a} a

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

IsLeast {a} a

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

IsLUB {a} a

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

IsGLB {a} a

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

BddAbove {a}

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

BddBelow {a}

@[simp]

theorem upperBounds_singleton {α : Type u} [inst : Preorder α] {a : α} :

upperBounds {a} = Set.Ici a

@[simp]

theorem lowerBounds_singleton {α : Type u} [inst : Preorder α] {a : α} :

lowerBounds {a} = Set.Iic a

Bounded intervals #

theorem bddAbove_Icc {α : Type u} [inst : Preorder α] {a : α} {b : α} :

BddAbove (Set.Icc a b)

theorem bddBelow_Icc {α : Type u} [inst : Preorder α] {a : α} {b : α} :

BddBelow (Set.Icc a b)

theorem bddAbove_Ico {α : Type u} [inst : Preorder α] {a : α} {b : α} :

BddAbove (Set.Ico a b)

theorem bddBelow_Ico {α : Type u} [inst : Preorder α] {a : α} {b : α} :

BddBelow (Set.Ico a b)

theorem bddAbove_Ioc {α : Type u} [inst : Preorder α] {a : α} {b : α} :

BddAbove (Set.Ioc a b)

theorem bddBelow_Ioc {α : Type u} [inst : Preorder α] {a : α} {b : α} :

BddBelow (Set.Ioc a b)

theorem bddAbove_Ioo {α : Type u} [inst : Preorder α] {a : α} {b : α} :

BddAbove (Set.Ioo a b)

theorem bddBelow_Ioo {α : Type u} [inst : Preorder α] {a : α} {b : α} :

BddBelow (Set.Ioo a b)

theorem isGreatest_Icc {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a ≤ b) :

IsGreatest (Set.Icc a b) b

theorem isLUB_Icc {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a ≤ b) :

IsLUB (Set.Icc a b) b

theorem upperBounds_Icc {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a ≤ b) :

upperBounds (Set.Icc a b) = Set.Ici b

theorem isLeast_Icc {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a ≤ b) :

IsLeast (Set.Icc a b) a

theorem isGLB_Icc {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a ≤ b) :

IsGLB (Set.Icc a b) a

theorem lowerBounds_Icc {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a ≤ b) :

lowerBounds (Set.Icc a b) = Set.Iic a

theorem isGreatest_Ioc {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < b) :

IsGreatest (Set.Ioc a b) b

theorem isLUB_Ioc {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < b) :

IsLUB (Set.Ioc a b) b

theorem upperBounds_Ioc {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < b) :

upperBounds (Set.Ioc a b) = Set.Ici b

theorem isLeast_Ico {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < b) :

IsLeast (Set.Ico a b) a

theorem isGLB_Ico {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < b) :

IsGLB (Set.Ico a b) a

theorem lowerBounds_Ico {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < b) :

lowerBounds (Set.Ico a b) = Set.Iic a

theorem isGLB_Ioo {γ : Type w} [inst : SemilatticeSup γ] [inst : DenselyOrdered γ] {a : γ} {b : γ} (h : a < b) :

IsGLB (Set.Ioo a b) a

theorem lowerBounds_Ioo {γ : Type w} [inst : SemilatticeSup γ] [inst : DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :

lowerBounds (Set.Ioo a b) = Set.Iic a

theorem isGLB_Ioc {γ : Type w} [inst : SemilatticeSup γ] [inst : DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :

IsGLB (Set.Ioc a b) a

theorem lowerBounds_Ioc {γ : Type w} [inst : SemilatticeSup γ] [inst : DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :

lowerBounds (Set.Ioc a b) = Set.Iic a

theorem isLUB_Ioo {γ : Type w} [inst : SemilatticeInf γ] [inst : DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :

IsLUB (Set.Ioo a b) b

theorem upperBounds_Ioo {γ : Type w} [inst : SemilatticeInf γ] [inst : DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :

upperBounds (Set.Ioo a b) = Set.Ici b

theorem isLUB_Ico {γ : Type w} [inst : SemilatticeInf γ] [inst : DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :

IsLUB (Set.Ico a b) b

theorem upperBounds_Ico {γ : Type w} [inst : SemilatticeInf γ] [inst : DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :

upperBounds (Set.Ico a b) = Set.Ici b

theorem bddBelow_iff_subset_Ici {α : Type u} [inst : Preorder α] {s : Set α} :

BddBelow s ↔ ∃ a, s ⊆ Set.Ici a

theorem bddAbove_iff_subset_Iic {α : Type u} [inst : Preorder α] {s : Set α} :

BddAbove s ↔ ∃ a, s ⊆ Set.Iic a

theorem bddBelow_bddAbove_iff_subset_Icc {α : Type u} [inst : Preorder α] {s : Set α} :

BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Set.Icc a b

Univ #

@[simp]

theorem isGreatest_univ_iff {α : Type u} [inst : Preorder α] {a : α} :

IsGreatest Set.univ a ↔ IsTop a

theorem isGreatest_univ {α : Type u} [inst : Preorder α] [inst : OrderTop α] :

IsGreatest Set.univ ⊤

@[simp]

theorem OrderTop.upperBounds_univ {γ : Type w} [inst : PartialOrder γ] [inst : OrderTop γ] :

upperBounds Set.univ = {⊤}

theorem isLUB_univ {α : Type u} [inst : Preorder α] [inst : OrderTop α] :

IsLUB Set.univ ⊤

@[simp]

theorem OrderBot.lowerBounds_univ {γ : Type w} [inst : PartialOrder γ] [inst : OrderBot γ] :

lowerBounds Set.univ = {⊥}

@[simp]

theorem isLeast_univ_iff {α : Type u} [inst : Preorder α] {a : α} :

IsLeast Set.univ a ↔ IsBot a

theorem isLeast_univ {α : Type u} [inst : Preorder α] [inst : OrderBot α] :

IsLeast Set.univ ⊥

theorem isGLB_univ {α : Type u} [inst : Preorder α] [inst : OrderBot α] :

IsGLB Set.univ ⊥

@[simp]

theorem NoMaxOrder.upperBounds_univ {α : Type u} [inst : Preorder α] [inst : NoMaxOrder α] :

upperBounds Set.univ = ∅

@[simp]

theorem NoMinOrder.lowerBounds_univ {α : Type u} [inst : Preorder α] [inst : NoMinOrder α] :

lowerBounds Set.univ = ∅

@[simp]

theorem not_bddAbove_univ {α : Type u} [inst : Preorder α] [inst : NoMaxOrder α] :

¬BddAbove Set.univ

@[simp]

theorem not_bddBelow_univ {α : Type u} [inst : Preorder α] [inst : NoMinOrder α] :

¬BddBelow Set.univ

Empty set #

@[simp]

theorem upperBounds_empty {α : Type u} [inst : Preorder α] :

upperBounds ∅ = Set.univ

@[simp]

theorem lowerBounds_empty {α : Type u} [inst : Preorder α] :

lowerBounds ∅ = Set.univ

@[simp]

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

BddAbove ∅

@[simp]

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

BddBelow ∅

@[simp]

theorem isGLB_empty_iff {α : Type u} [inst : Preorder α] {a : α} :

IsGLB ∅ a ↔ IsTop a

@[simp]

theorem isLUB_empty_iff {α : Type u} [inst : Preorder α] {a : α} :

IsLUB ∅ a ↔ IsBot a

theorem isGLB_empty {α : Type u} [inst : Preorder α] [inst : OrderTop α] :

IsGLB ∅ ⊤

theorem isLUB_empty {α : Type u} [inst : Preorder α] [inst : OrderBot α] :

IsLUB ∅ ⊥

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

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

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

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

insert #

@[simp]

theorem bddAbove_insert {γ : Type w} [inst : SemilatticeSup γ] (a : γ) {s : Set γ} :

BddAbove (insert a s) ↔ BddAbove s

Adding a point to a set preserves its boundedness above.

theorem BddAbove.insert {γ : Type w} [inst : SemilatticeSup γ] (a : γ) {s : Set γ} (hs : BddAbove s) :

BddAbove (insert a s)

@[simp]

theorem bddBelow_insert {γ : Type w} [inst : SemilatticeInf γ] (a : γ) {s : Set γ} :

BddBelow (insert a s) ↔ BddBelow s

Adding a point to a set preserves its boundedness below.

theorem BddBelow.insert {γ : Type w} [inst : SemilatticeInf γ] (a : γ) {s : Set γ} (hs : BddBelow s) :

BddBelow (insert a s)

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

IsLUB (insert a s) (a ⊔ b)

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

IsGLB (insert a s) (a ⊓ b)

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

IsGreatest (insert a s) (max a b)

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

IsLeast (insert a s) (min a b)

@[simp]

theorem upperBounds_insert {α : Type u} [inst : Preorder α] (a : α) (s : Set α) :

upperBounds (insert a s) = Set.Ici a ∩ upperBounds s

@[simp]

theorem lowerBounds_insert {α : Type u} [inst : Preorder α] (a : α) (s : Set α) :

lowerBounds (insert a s) = Set.Iic a ∩ lowerBounds s

@[simp]

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

BddAbove s

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

@[simp]

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

BddBelow s

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

Pair #

theorem isLUB_pair {γ : Type w} [inst : SemilatticeSup γ] {a : γ} {b : γ} :

IsLUB {a, b} (a ⊔ b)

theorem isGLB_pair {γ : Type w} [inst : SemilatticeInf γ] {a : γ} {b : γ} :

IsGLB {a, b} (a ⊓ b)

theorem isLeast_pair {γ : Type w} [inst : LinearOrder γ] {a : γ} {b : γ} :

IsLeast {a, b} (min a b)

theorem isGreatest_pair {γ : Type w} [inst : LinearOrder γ] {a : γ} {b : γ} :

IsGreatest {a, b} (max a b)

Lower/upper bounds #

@[simp]

theorem isLUB_lowerBounds {α : Type u} [inst : Preorder α] {s : Set α} {a : α} :

IsLUB (lowerBounds s) a ↔ IsGLB s a

@[simp]

theorem isGLB_upperBounds {α : Type u} [inst : 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} [inst : Preorder α] {s : Set α} {a : α} {b : α} (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s) :

Set.Nonempty s → a ≤ b

theorem isGLB_le_isLUB {α : Type u} [inst : 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} [inst : Preorder α] {s : Set α} {a : α} {b : α} (ha : IsLUB s a) :

a < b ↔ ∃ c, c ∈ upperBounds s ∧ c < b

theorem lt_isGLB_iff {α : Type u} [inst : 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} [inst : 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} [inst : PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsLeast s a) (Hb : IsLeast s b) :

a = b

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

IsLeast s b ↔ a = b

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

a = b

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

IsGreatest s b ↔ a = b

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

a = b

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

a = b

theorem Set.subsingleton_of_isLUB_le_isGLB {α : Type u} [inst : 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} [inst : 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} [inst : LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) :

b < a ↔ ∃ c, c ∈ s ∧ b < c

theorem isGLB_lt_iff {α : Type u} [inst : LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) :

a < b ↔ ∃ c, c ∈ s ∧ c < b

theorem IsLUB.exists_between {α : Type u} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : Preorder β] {f : α → β} (Hf : Monotone f) {s : Set α} :

f '' upperBounds s ⊆ upperBounds (f '' s)

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

f '' lowerBounds s ⊆ lowerBounds (f '' s)

theorem Monotone.map_bddAbove {α : Type u} {β : Type v} [inst : Preorder α] [inst : 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 bdd_above.image2.

theorem Monotone.map_bddBelow {α : Type u} {β : Type v} [inst : Preorder α] [inst : 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 bdd_below.image2.

theorem Monotone.map_isLeast {α : Type u} {β : Type v} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : Preorder β] {f : α → β} (hf : Antitone f) {s : Set α} :

f '' lowerBounds s ⊆ upperBounds (f '' s)

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

f '' upperBounds s ⊆ lowerBounds (f '' s)

theorem Antitone.map_bddAbove {α : Type u} {β : Type v} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : 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)