Documentation

Mathlib.Order.Bounds.Basic

Upper / lower bounds #

In this file we define:

Definitions #

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

The set of upper bounds of a set.

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

The set of lower bounds of a set.

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

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

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

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

Equations
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
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
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
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
theorem mem_upperBounds {α : Type u} [inst : Preorder α] {s : Set α} {a : α} :
a upperBounds s ∀ (x : α), x sx a
theorem mem_lowerBounds {α : Type u} [inst : Preorder α] {s : Set α} {a : α} :
a lowerBounds s ∀ (x : α), x sa x
theorem bddAbove_def {α : Type u} [inst : Preorder α] {s : Set α} :
BddAbove s x, ∀ (y : α), y sy x
theorem bddBelow_def {α : Type u} [inst : Preorder α] {s : Set α} :
BddBelow s x, ∀ (y : α), y sx y
theorem bot_mem_lowerBounds {α : Type u} [inst : Preorder α] [inst : OrderBot α] (s : Set α) :
theorem top_mem_upperBounds {α : Type u} [inst : Preorder α] [inst : OrderTop α] (s : Set α) :
@[simp]
theorem isLeast_bot_iff {α : Type u} [inst : Preorder α] {s : Set α} [inst : OrderBot α] :
@[simp]
theorem isGreatest_top_iff {α : Type u} [inst : Preorder α] {s : Set α} [inst : OrderTop α] :
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) :

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

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

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

Equations

Monotonicity #

theorem upperBounds_mono_set {α : Type u} [inst : Preorder α] ⦃s : Set α ⦃t : Set α (hst : s t) :
theorem lowerBounds_mono_set {α : Type u} [inst : Preorder α] ⦃s : Set α ⦃t : Set α (hst : s t) :
theorem upperBounds_mono_mem {α : Type u} [inst : Preorder α] {s : Set α} ⦃a : α ⦃b : α (hab : a b) :
theorem lowerBounds_mono_mem {α : Type u} [inst : Preorder α] {s : Set α} ⦃a : α ⦃b : α (hab : a b) :
theorem upperBounds_mono {α : Type u} [inst : Preorder α] ⦃s : Set α ⦃t : Set α (hst : s t) ⦃a : α ⦃b : α (hab : a b) :
theorem lowerBounds_mono {α : Type u} [inst : Preorder α] ⦃s : Set α ⦃t : Set α (hst : s t) ⦃a : α ⦃b : α (hab : a b) :
theorem BddAbove.mono {α : Type u} [inst : Preorder α] ⦃s : Set α ⦃t : Set α (h : s t) :

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) :

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

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) :
theorem IsGLB.lowerBounds_eq {α : Type u} [inst : Preorder α] {s : Set α} {a : α} (h : IsGLB s a) :
theorem IsLeast.lowerBounds_eq {α : Type u} [inst : Preorder α] {s : Set α} {a : α} (h : IsLeast s a) :
theorem IsGreatest.upperBounds_eq {α : Type u} [inst : Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) :
theorem IsGreatest.lt_iff {α : Type u} [inst : Preorder α] {s : Set α} {a : α} {b : α} (h : IsGreatest s a) :
a < b ∀ (x : α), x sx < b
theorem IsLeast.lt_iff {α : Type u} [inst : Preorder α] {s : Set α} {a : α} {b : α} (h : IsLeast s a) :
b < a ∀ (x : α), x sb < x
theorem isLUB_le_iff {α : Type u} [inst : Preorder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) :
theorem le_isGLB_iff {α : Type u} [inst : Preorder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) :
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) :

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) :

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) :

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) :

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 α} :
@[simp]
theorem lowerBounds_union {α : Type u} [inst : Preorder α] {s : Set α} {t : Set α} :
theorem isLeast_union_iff {α : Type u} [inst : Preorder α] {a : α} {s : Set α} {t : Set α} :
theorem isGreatest_union_iff {α : Type u} [inst : Preorder α] {s : Set α} {t : Set α} {a : α} :
theorem BddAbove.inter_of_left {α : Type u} [inst : Preorder α] {s : Set α} {t : Set α} (h : BddAbove s) :

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) :

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) :

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) :

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

theorem BddAbove.union {γ : Type w} [inst : SemilatticeSup γ] {s : Set γ} {t : Set γ} :
BddAbove sBddAbove tBddAbove (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 γ} :

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 sBddBelow tBddBelow (s t)
theorem bddBelow_union {γ : Type w} [inst : SemilatticeInf γ] {s : Set γ} {t : Set γ} :

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 sy x
theorem bddBelow_iff_exists_le {γ : Type w} [inst : SemilatticeInf γ] {s : Set γ} (x₀ : γ) :
BddBelow s x, x x₀ ∀ (y : γ), y sx y
theorem BddAbove.exists_ge {γ : Type w} [inst : SemilatticeSup γ] {s : Set γ} (hs : BddAbove s) (x₀ : γ) :
x, x₀ x ∀ (y : γ), y sy x
theorem BddBelow.exists_le {γ : Type w} [inst : SemilatticeInf γ] {s : Set γ} (hs : BddBelow s) (x₀ : γ) :
x, x x₀ ∀ (y : γ), y sx y

Specific sets #

Unbounded intervals #

theorem isLeast_Ici {α : Type u} [inst : Preorder α] {a : α} :
theorem isGreatest_Iic {α : Type u} [inst : Preorder α] {a : α} :
theorem isLUB_Iic {α : Type u} [inst : Preorder α] {a : α} :
theorem isGLB_Ici {α : Type u} [inst : Preorder α] {a : α} :
theorem upperBounds_Iic {α : Type u} [inst : Preorder α] {a : α} :
theorem lowerBounds_Ici {α : Type u} [inst : Preorder α] {a : α} :
theorem bddAbove_Iic {α : Type u} [inst : Preorder α] {a : α} :
theorem bddBelow_Ici {α : Type u} [inst : Preorder α] {a : α} :
theorem bddAbove_Iio {α : Type u} [inst : Preorder α] {a : α} :
theorem bddBelow_Ioi {α : Type u} [inst : Preorder α] {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) :
theorem glb_Ioi_eq_self_or_Ioi_eq_Ici {γ : Type w} [inst : PartialOrder γ] {j : γ} (i : γ) (hj : IsGLB (Set.Ioi i) 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 : γ} :
theorem isGLB_Ioi {γ : Type w} [inst : LinearOrder γ] [inst : DenselyOrdered γ] {a : γ} :
theorem upperBounds_Iio {γ : Type w} [inst : LinearOrder γ] [inst : DenselyOrdered γ] {a : γ} :
theorem lowerBounds_Ioi {γ : Type w} [inst : LinearOrder γ] [inst : DenselyOrdered γ] {a : γ} :

Singleton #

theorem isGreatest_singleton {α : Type u} [inst : Preorder α] {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 : α} :
theorem bddBelow_singleton {α : Type u} [inst : Preorder α] {a : α} :
@[simp]
theorem upperBounds_singleton {α : Type u} [inst : Preorder α] {a : α} :
@[simp]
theorem lowerBounds_singleton {α : Type u} [inst : Preorder α] {a : α} :

Bounded intervals #

theorem bddAbove_Icc {α : Type u} [inst : Preorder α] {a : α} {b : α} :
theorem bddBelow_Icc {α : Type u} [inst : Preorder α] {a : α} {b : α} :
theorem bddAbove_Ico {α : Type u} [inst : Preorder α] {a : α} {b : α} :
theorem bddBelow_Ico {α : Type u} [inst : Preorder α] {a : α} {b : α} :
theorem bddAbove_Ioc {α : Type u} [inst : Preorder α] {a : α} {b : α} :
theorem bddBelow_Ioc {α : Type u} [inst : Preorder α] {a : α} {b : α} :
theorem bddAbove_Ioo {α : Type u} [inst : Preorder α] {a : α} {b : α} :
theorem bddBelow_Ioo {α : Type u} [inst : Preorder α] {a : α} {b : α} :
theorem isGreatest_Icc {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a 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) :
theorem isLeast_Icc {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a b) :
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) :
theorem isGreatest_Ioc {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < 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) :
theorem isLeast_Ico {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < b) :
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) :
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) :
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) :
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) :
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) :
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 α] :
@[simp]
theorem bddBelow_empty {α : Type u} [inst : Preorder α] [inst : Nonempty α] :
@[simp]
theorem isGLB_empty_iff {α : Type u} [inst : Preorder α] {a : α} :
@[simp]
theorem isLUB_empty_iff {α : Type u} [inst : Preorder α] {a : α} :
theorem isGLB_empty {α : Type u} [inst : Preorder α] [inst : OrderTop α] :
theorem isLUB_empty {α : Type u} [inst : Preorder α] [inst : OrderBot α] :
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 γ} :

Adding a point to a set preserves its boundedness above.

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

Adding a point to a set preserves its boundedness below.

theorem BddBelow.insert {γ : Type w} [inst : SemilatticeInf γ] (a : γ) {s : Set γ} (hs : BddBelow 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 α) :
@[simp]
theorem lowerBounds_insert {α : Type u} [inst : Preorder α] (a : α) (s : Set α) :
@[simp]
theorem OrderTop.bddAbove {α : Type u} [inst : Preorder α] [inst : OrderTop α] (s : Set α) :

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

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

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 : α} :
@[simp]
theorem isGLB_upperBounds {α : Type u} [inst : Preorder α] {s : Set α} {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 sa 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) :
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 ta tf 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 ta tf 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) :
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) :
theorem MonotoneOn.map_bddAbove {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) (Hst : s t) :

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) :

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 tf 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 ta tf 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 sa tf 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 ta tf 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) :
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) :
theorem AntitoneOn.map_bddAbove {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) (Hst : s t) :

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) :

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 aIsLeast (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 aIsGreatest (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 α} :
theorem Monotone.image_lowerBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {f : αβ} (Hf : Monotone f) {s : Set α} :
theorem Monotone.map_bddAbove {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {f : αβ} (Hf : Monotone f) {s : Set α} :
BddAbove sBddAbove (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 sBddBelow (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 sf 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 sf 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 α} :
theorem Antitone.image_upperBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {f : αβ} (hf : Antitone f) {s : Set α} :
theorem Antitone.map_bddAbove {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {f : αβ} (hf : Antitone f) {s : Set α} :
BddAbove sBddBelow (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 sBddAbove (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 aIsLeast (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 aIsGreatest (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)) :
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)) :
theorem BddAbove.image2 {α : 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)) :
BddAbove sBddAbove tBddAbove (Set.image2 f s t)

See also Monotone.map_bddAbove.

theorem BddBelow.image2 {α : 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)) :
BddBelow sBddBelow tBddBelow (Set.image2 f s t)

See also Monotone.map_bddBelow.

theorem IsGreatest.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 : 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} [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 : 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} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
theorem image2_lowerBounds_upperBounds_subset_lowerBounds_image2 {α : 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 : α), Antitone (f a)) :
theorem BddAbove.bddAbove_image2_of_bddBelow {α : 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 : α), Antitone (f a)) :
BddAbove sBddBelow tBddAbove (Set.image2 f s t)
theorem BddBelow.bddBelow_image2_of_bddAbove {α : 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 : α), Antitone (f a)) :
BddBelow sBddAbove tBddBelow (Set.image2 f s t)
theorem IsGreatest.isGreatest_image2_of_isLeast {α : 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 : α), 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} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
theorem image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
theorem BddBelow.image2_bddAbove {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
BddBelow sBddBelow tBddAbove (Set.image2 f s t)
theorem BddAbove.image2_bddBelow {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
BddAbove sBddAbove tBddBelow (Set.image2 f s t)
theorem IsLeast.isGreatest_image2 {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) :
theorem image2_upperBounds_lowerBounds_subset_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) :
theorem BddBelow.bddAbove_image2_of_bddAbove {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) :
BddBelow sBddAbove tBddAbove (Set.image2 f s t)
theorem BddAbove.bddBelow_image2_of_bddAbove {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) :
BddAbove sBddBelow tBddBelow (Set.image2 f s t)
theorem IsLeast.isGreatest_image2_of_isGreatest {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst : Preorder β] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : 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 IsGLB.of_image {α : Type u} {β : Type v} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : 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_pi {α : Type u} {π : αType u_1} [inst : (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} [inst : (a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} {f : (a : α) → π a} :
IsGLB s f ∀ (a : α), IsGLB (Function.eval a '' s) (f a)
theorem isLUB_prod {α : Type u} {β : Type v} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : Preorder β] {s : Set (α × β)} (p : α × β) :
IsGLB s p IsGLB (Prod.fst '' s) p.fst IsGLB (Prod.snd '' s) p.snd