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:
upper_bounds,lower_bounds: the set of upper bounds (resp., lower bounds) of a set;bdd_above s,bdd_below s: the setsis bounded above (resp., below), i.e., the set of upper (resp., lower) bounds ofsis nonempty;is_least s a,is_greatest s a:ais a least (resp., greatest) element ofs; for a partial order, it is unique if exists;is_lub s a,is_glb s a:ais a least upper bound (resp., a greatest lower bound) ofs; for a partial order, it is unique if exists.
We also prove various lemmas about monotonicity, behaviour under ∪, ∩, insert, and provide
formulas for ∅, univ, and intervals.
Definitions #
a is a greatest element of a set s; for a partial order, it is unique if exists
Equations
- is_greatest s a = (a ∈ s ∧ a ∈ upper_bounds s)
a is a greatest lower bound of a set s; for a partial order, it is unique if exists.
Equations
- is_glb s = is_greatest (lower_bounds s)
theorem
bot_mem_lower_bounds
{α : Type u}
[preorder α]
[order_bot α]
(s : set α) :
⊥ ∈ lower_bounds s
theorem
top_mem_upper_bounds
{α : Type u}
[preorder α]
[order_top α]
(s : set α) :
⊤ ∈ upper_bounds s
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.
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.
Monotonicity #
theorem
upper_bounds_mono_mem
{α : Type u}
[preorder α]
{s : set α}
⦃a b : α⦄
(hab : a ≤ b) :
a ∈ upper_bounds s → b ∈ upper_bounds s
theorem
lower_bounds_mono_mem
{α : Type u}
[preorder α]
{s : set α}
⦃a b : α⦄
(hab : a ≤ b) :
b ∈ lower_bounds s → a ∈ lower_bounds s
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
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
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
theorem
subset_lower_bounds_upper_bounds
{α : Type u}
[preorder α]
(s : set α) :
s ⊆ lower_bounds (upper_bounds s)
theorem
subset_upper_bounds_lower_bounds
{α : Type u}
[preorder α]
(s : set α) :
s ⊆ upper_bounds (lower_bounds s)
theorem
set.nonempty.bdd_above_lower_bounds
{α : Type u}
[preorder α]
{s : set α}
(hs : s.nonempty) :
theorem
set.nonempty.bdd_below_upper_bounds
{α : Type u}
[preorder α]
{s : set α}
(hs : s.nonempty) :
Conversions #
theorem
is_greatest.is_lub
{α : Type u}
[preorder α]
{s : set α}
{a : α}
(h : is_greatest s a) :
is_lub s a
theorem
is_lub.upper_bounds_eq
{α : Type u}
[preorder α]
{s : set α}
{a : α}
(h : is_lub s a) :
upper_bounds s = set.Ici a
theorem
is_glb.lower_bounds_eq
{α : Type u}
[preorder α]
{s : set α}
{a : α}
(h : is_glb s a) :
lower_bounds s = set.Iic a
theorem
is_least.lower_bounds_eq
{α : Type u}
[preorder α]
{s : set α}
{a : α}
(h : is_least s a) :
lower_bounds s = set.Iic a
theorem
is_greatest.upper_bounds_eq
{α : Type u}
[preorder α]
{s : set α}
{a : α}
(h : is_greatest s a) :
upper_bounds s = set.Ici a
theorem
is_lub_le_iff
{α : Type u}
[preorder α]
{s : set α}
{a b : α}
(h : is_lub s a) :
a ≤ b ↔ b ∈ upper_bounds s
theorem
le_is_glb_iff
{α : Type u}
[preorder α]
{s : set α}
{a b : α}
(h : is_glb s a) :
b ≤ a ↔ b ∈ lower_bounds s
If s has a greatest element, then it is bounded above.
theorem
is_greatest.nonempty
{α : Type u}
[preorder α]
{s : set α}
{a : α}
(h : is_greatest s a) :
s.nonempty
Union and intersection #
@[simp]
theorem
upper_bounds_union
{α : Type u}
[preorder α]
{s t : set α} :
upper_bounds (s ∪ t) = upper_bounds s ∩ upper_bounds t
@[simp]
theorem
lower_bounds_union
{α : Type u}
[preorder α]
{s t : set α} :
lower_bounds (s ∪ t) = lower_bounds s ∩ lower_bounds t
theorem
union_upper_bounds_subset_upper_bounds_inter
{α : Type u}
[preorder α]
{s t : set α} :
upper_bounds s ∪ upper_bounds t ⊆ upper_bounds (s ∩ t)
theorem
union_lower_bounds_subset_lower_bounds_inter
{α : Type u}
[preorder α]
{s t : set α} :
lower_bounds s ∪ lower_bounds t ⊆ lower_bounds (s ∩ t)
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
If s and t are bounded above sets in a semilattice_sup, then so is s ∪ t.
theorem
is_lub.union
{γ : Type w}
[semilattice_sup γ]
{a b : γ}
{s t : set γ}
(hs : is_lub s a)
(ht : is_lub t b) :
If a is the least upper bound of s and b is the least upper bound of t,
then a ⊔ b is the least upper bound of s ∪ t.
theorem
is_glb.union
{γ : Type w}
[semilattice_inf γ]
{a₁ a₂ : γ}
{s t : set γ}
(hs : is_glb s a₁)
(ht : is_glb t a₂) :
If a is the greatest lower bound of s and b is the greatest lower bound of t,
then a ⊓ b is the greatest lower bound of s ∪ t.
theorem
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.
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.
theorem
is_lub.inter_Ici_of_mem
{γ : Type w}
[linear_order γ]
{s : set γ}
{a b : γ}
(ha : is_lub s a)
(hb : b ∈ s) :
theorem
is_glb.inter_Iic_of_mem
{γ : Type w}
[linear_order γ]
{s : set γ}
{a b : γ}
(ha : is_glb s a)
(hb : b ∈ s) :
theorem
upper_bounds_Iio
{γ : Type w}
[linear_order γ]
[densely_ordered γ]
{a : γ} :
upper_bounds (set.Iio a) = set.Ici a
theorem
lower_bounds_Ioi
{γ : Type w}
[linear_order γ]
[densely_ordered γ]
{a : γ} :
lower_bounds (set.Ioi a) = set.Iic a
Singleton #
@[simp]
@[simp]
Bounded intervals #
theorem
is_greatest_Icc
{α : Type u}
[preorder α]
{a b : α}
(h : a ≤ b) :
is_greatest (set.Icc a b) b
theorem
upper_bounds_Icc
{α : Type u}
[preorder α]
{a b : α}
(h : a ≤ b) :
upper_bounds (set.Icc a b) = set.Ici b
theorem
lower_bounds_Icc
{α : Type u}
[preorder α]
{a b : α}
(h : a ≤ b) :
lower_bounds (set.Icc a b) = set.Iic a
theorem
is_greatest_Ioc
{α : Type u}
[preorder α]
{a b : α}
(h : a < b) :
is_greatest (set.Ioc a b) b
theorem
upper_bounds_Ioc
{α : Type u}
[preorder α]
{a b : α}
(h : a < b) :
upper_bounds (set.Ioc a b) = set.Ici b
theorem
lower_bounds_Ico
{α : Type u}
[preorder α]
{a b : α}
(h : a < b) :
lower_bounds (set.Ico a b) = set.Iic a
theorem
lower_bounds_Ioo
{γ : Type w}
[semilattice_sup γ]
[densely_ordered γ]
{a b : γ}
(hab : a < b) :
lower_bounds (set.Ioo a b) = set.Iic a
theorem
lower_bound_Ioc
{γ : Type w}
[semilattice_sup γ]
[densely_ordered γ]
{a b : γ}
(hab : a < b) :
lower_bounds (set.Ioc a b) = set.Iic a
theorem
upper_bounds_Ioo
{γ : Type w}
[semilattice_inf γ]
[densely_ordered γ]
{a b : γ}
(hab : a < b) :
upper_bounds (set.Ioo a b) = set.Ici b
theorem
upper_bounds_Ico
{γ : Type w}
[semilattice_inf γ]
[densely_ordered γ]
{a b : γ}
(hab : a < b) :
upper_bounds (set.Ico a b) = set.Ici b
Univ #
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Empty set #
theorem
is_lub.nonempty
{α : Type u}
[preorder α]
{s : set α}
{a : α}
[no_min_order α]
(hs : is_lub s a) :
s.nonempty
theorem
is_glb.nonempty
{α : Type u}
[preorder α]
{s : set α}
{a : α}
[no_max_order α]
(hs : is_glb s a) :
s.nonempty
insert #
@[simp]
theorem
bdd_above_insert
{γ : Type w}
[semilattice_sup γ]
(a : γ)
{s : set γ} :
bdd_above (has_insert.insert a s) ↔ bdd_above s
Adding a point to a set preserves its boundedness above.
theorem
bdd_above.insert
{γ : Type w}
[semilattice_sup γ]
(a : γ)
{s : set γ}
(hs : bdd_above s) :
bdd_above (has_insert.insert a s)
@[simp]
theorem
bdd_below_insert
{γ : Type w}
[semilattice_inf γ]
(a : γ)
{s : set γ} :
bdd_below (has_insert.insert a s) ↔ bdd_below s
Adding a point to a set preserves its boundedness below.
theorem
bdd_below.insert
{γ : Type w}
[semilattice_inf γ]
(a : γ)
{s : set γ}
(hs : bdd_below s) :
bdd_below (has_insert.insert a s)
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)
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)
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)
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)
@[simp]
theorem
upper_bounds_insert
{α : Type u}
[preorder α]
(a : α)
(s : set α) :
upper_bounds (has_insert.insert a s) = set.Ici a ∩ upper_bounds s
@[simp]
theorem
lower_bounds_insert
{α : Type u}
[preorder α]
(a : α)
(s : set α) :
lower_bounds (has_insert.insert a s) = set.Iic a ∩ lower_bounds s
Pair #
theorem
is_least_pair
{γ : Type w}
[linear_order γ]
{a b : γ} :
is_least {a, b} (linear_order.min a b)
theorem
is_greatest_pair
{γ : Type w}
[linear_order γ]
{a b : γ} :
is_greatest {a, b} (linear_order.max a b)
Lower/upper bounds #
@[simp]
theorem
is_lub_lower_bounds
{α : Type u}
[preorder α]
{s : set α}
{a : α} :
is_lub (lower_bounds s) a ↔ is_glb s a
@[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 #
theorem
lower_bounds_le_upper_bounds
{α : Type u}
[preorder α]
{s : set α}
{a b : α}
(ha : a ∈ lower_bounds s)
(hb : b ∈ upper_bounds s) :
theorem
is_least.unique
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_least s a)
(Hb : is_least s b) :
a = b
theorem
is_least.is_least_iff_eq
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_least s a) :
theorem
is_greatest.unique
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_greatest s a)
(Hb : is_greatest s b) :
a = b
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
theorem
is_lub.unique
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_lub s a)
(Hb : is_lub s b) :
a = b
theorem
is_glb.unique
{α : Type u}
[partial_order α]
{s : set α}
{a b : α}
(Ha : is_glb s a)
(Hb : is_glb s b) :
a = b
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) :
Images of upper/lower bounds under monotone functions #
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)
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)
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)
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)
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)
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)
theorem
monotone_on.map_bdd_above
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s t : set α}
(Hf : monotone_on 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
monotone_on.map_bdd_below
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
{s t : set α}
(Hf : monotone_on 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
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.
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)
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)
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)
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)
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)
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)
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.
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.
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)
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)
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)
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)
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.
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)