doc-next-gen

Mathlib.Order.Bounds.Image

Module docstring

{"# Images of upper/lower bounds under monotone functions

In this file we prove various results about the behaviour of bounds under monotone/antitone maps. "}

MonotoneOn.mem_upperBounds_image theorem
(Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ upperBounds s) (Hat : a ∈ t) : f a ∈ upperBounds (f '' s)
Full source 
theorem mem_upperBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ upperBounds s)
    (Hat : a ∈ t) : f a ∈ upperBounds (f '' s) :=
  forall_mem_image.2 fun _ H => Hf (Hst H) Hat (Has H)
Monotone Functions Preserve Upper Bounds on Subsets
Informal description
Let $f$ be a function defined on a set $t$ in a preordered type $\alpha$, and let $s$ be a subset of $t$. If $f$ is monotone on $t$, $a$ is an upper bound for $s$, and $a \in t$, then $f(a)$ is an upper bound for the image $f(s)$.
MonotoneOn.mem_upperBounds_image_self theorem
(Hf : MonotoneOn f t) : a ∈ upperBounds t → a ∈ t → f a ∈ upperBounds (f '' t)
Full source 
theorem mem_upperBounds_image_self (Hf : MonotoneOn f t) :
    a ∈ upperBounds t → a ∈ t → f a ∈ upperBounds (f '' t) :=
  Hf.mem_upperBounds_image subset_rfl
Monotone Functions Preserve Upper Bounds on Their Domain
Informal description
Let $f$ be a function defined on a set $t$ in a preordered type $\alpha$, and suppose $f$ is monotone on $t$. If $a$ is an upper bound for $t$ and $a \in t$, then $f(a)$ is an upper bound for the image $f(t)$.
MonotoneOn.mem_lowerBounds_image theorem
(Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) (Hat : a ∈ t) : f a ∈ lowerBounds (f '' s)
Full source 
theorem mem_lowerBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s)
    (Hat : a ∈ t) : f a ∈ lowerBounds (f '' s) :=
  forall_mem_image.2 fun _ H => Hf Hat (Hst H) (Has H)
Monotone Function Preserves Lower Bounds on Subset
Informal description
Let $f$ be a function defined on a set $t$ in a partially ordered type, and let $s$ be a subset of $t$. If $f$ is monotone on $t$, $a$ is a lower bound of $s$, and $a$ belongs to $t$, then $f(a)$ is a lower bound of the image $f(s)$.
MonotoneOn.mem_lowerBounds_image_self theorem
(Hf : MonotoneOn f t) : a ∈ lowerBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)
Full source 
theorem mem_lowerBounds_image_self (Hf : MonotoneOn f t) :
    a ∈ lowerBounds t → a ∈ t → f a ∈ lowerBounds (f '' t) :=
  Hf.mem_lowerBounds_image subset_rfl
Monotone Function Preserves Lower Bounds on Its Domain
Informal description
Let $f$ be a function defined on a set $t$ in a partially ordered type, and suppose $f$ is monotone on $t$. If $a$ is a lower bound for $t$ and $a \in t$, then $f(a)$ is a lower bound for the image $f(t)$.
MonotoneOn.image_upperBounds_subset_upperBounds_image theorem
(Hf : MonotoneOn f t) (Hst : s ⊆ t) : f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)
Full source 
theorem image_upperBounds_subset_upperBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) :
    f '' (upperBounds s ∩ t)f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s) := by
  rintro _ ⟨a, ha, rfl⟩
  exact Hf.mem_upperBounds_image Hst ha.1 ha.2
Monotone Functions Preserve Upper Bounds on Images
Informal description
Let $f$ be a function defined on a set $t$ in a preordered type $\alpha$, and let $s$ be a subset of $t$. If $f$ is monotone on $t$, then the image under $f$ of the intersection of $t$ with the upper bounds of $s$ is contained in the set of upper bounds of the image $f(s)$. In other words, for any $a \in t$ that is an upper bound for $s$, $f(a)$ is an upper bound for $f(s)$.
MonotoneOn.image_lowerBounds_subset_lowerBounds_image theorem
(Hf : MonotoneOn f t) (Hst : s ⊆ t) : f '' (lowerBounds s ∩ t) ⊆ lowerBounds (f '' s)
Full source 
theorem image_lowerBounds_subset_lowerBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) :
    f '' (lowerBounds s ∩ t)f '' (lowerBounds s ∩ t) ⊆ lowerBounds (f '' s) :=
  Hf.dual.image_upperBounds_subset_upperBounds_image Hst
Monotone Functions Preserve Lower Bounds on Images
Informal description
Let $f$ be a function defined on a set $t$ in a partially ordered type, and let $s$ be a subset of $t$. If $f$ is monotone on $t$, then the image under $f$ of the intersection of $t$ with the lower bounds of $s$ is contained in the set of lower bounds of the image $f(s)$. In other words, for any $a \in t$ that is a lower bound for $s$, $f(a)$ is a lower bound for $f(s)$.
MonotoneOn.map_bddAbove theorem
(Hf : MonotoneOn f t) (Hst : s ⊆ t) : (upperBounds s ∩ t).Nonempty → BddAbove (f '' s)
Full source 
/-- The image under a monotone function on a set `t` of a subset which has an upper bound in `t`
  is bounded above. -/
theorem map_bddAbove (Hf : MonotoneOn f t) (Hst : s ⊆ t) :
    (upperBoundsupperBounds s ∩ t).Nonempty → BddAbove (f '' s) := fun ⟨C, hs, ht⟩ =>
  ⟨f C, Hf.mem_upperBounds_image Hst hs ht⟩
Monotone functions preserve boundedness above on subsets
Informal description
Let $f$ be a function defined on a set $t$ in a preordered type $\alpha$, and let $s$ be a subset of $t$. If $f$ is monotone on $t$ and there exists an element in $t$ that is an upper bound for $s$, then the image $f(s)$ is bounded above.
MonotoneOn.map_bddBelow theorem
(Hf : MonotoneOn f t) (Hst : s ⊆ t) : (lowerBounds s ∩ t).Nonempty → BddBelow (f '' s)
Full source 
/-- The image under a monotone function on a set `t` of a subset which has a lower bound in `t`
  is bounded below. -/
theorem map_bddBelow (Hf : MonotoneOn f t) (Hst : s ⊆ t) :
    (lowerBoundslowerBounds s ∩ t).Nonempty → BddBelow (f '' s) := fun ⟨C, hs, ht⟩ =>
  ⟨f C, Hf.mem_lowerBounds_image Hst hs ht⟩
Monotone functions preserve boundedness below on subsets
Informal description
Let $f$ be a function defined on a set $t$ in a partially ordered type, and let $s$ be a subset of $t$. If $f$ is monotone on $t$ and there exists a lower bound of $s$ that belongs to $t$, then the image $f(s)$ is bounded below.
MonotoneOn.map_isLeast theorem
(Hf : MonotoneOn f t) (Ha : IsLeast t a) : IsLeast (f '' t) (f a)
Full source 
/-- A monotone map sends a least element of a set to a least element of its image. -/
theorem map_isLeast (Hf : MonotoneOn f t) (Ha : IsLeast t a) : IsLeast (f '' t) (f a) :=
  ⟨mem_image_of_mem _ Ha.1, Hf.mem_lowerBounds_image_self Ha.2 Ha.1⟩
Monotone Function Preserves Least Elements
Informal description
Let $f$ be a function defined on a set $t$ in a partially ordered type, and suppose $f$ is monotone on $t$. If $a$ is the least element of $t$, then $f(a)$ is the least element of the image $f(t)$.
MonotoneOn.map_isGreatest theorem
(Hf : MonotoneOn f t) (Ha : IsGreatest t a) : IsGreatest (f '' t) (f a)
Full source 
/-- A monotone map sends a greatest element of a set to a greatest element of its image. -/
theorem map_isGreatest (Hf : MonotoneOn f t) (Ha : IsGreatest t a) : IsGreatest (f '' t) (f a) :=
  ⟨mem_image_of_mem _ Ha.1, Hf.mem_upperBounds_image_self Ha.2 Ha.1⟩
Monotone Function Preserves Greatest Elements
Informal description
Let $f$ be a function defined on a set $t$ in a partially ordered type, and suppose $f$ is monotone on $t$. If $a$ is the greatest element of $t$, then $f(a)$ is the greatest element of the image $f(t)$.
AntitoneOn.mem_upperBounds_image theorem
(Hf : AntitoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) : a ∈ t → f a ∈ upperBounds (f '' s)
Full source 
theorem mem_upperBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) :
    a ∈ t → f a ∈ upperBounds (f '' s) :=
  Hf.dual_right.mem_lowerBounds_image Hst Has
Antitone Functions Map Lower Bounds to Upper Bounds of Subset Images
Informal description
Let $f$ be a function defined on a set $t$ in a preordered type, and let $s$ be a subset of $t$. If $f$ is antitone on $t$, $a$ is a lower bound of $s$, and $a \in t$, then $f(a)$ is an upper bound of the image $f(s)$.
AntitoneOn.mem_upperBounds_image_self theorem
(Hf : AntitoneOn f t) : a ∈ lowerBounds t → a ∈ t → f a ∈ upperBounds (f '' t)
Full source 
theorem mem_upperBounds_image_self (Hf : AntitoneOn f t) :
    a ∈ lowerBounds t → a ∈ t → f a ∈ upperBounds (f '' t) :=
  Hf.dual_right.mem_lowerBounds_image_self
Antitone Functions Map Lower Bounds to Upper Bounds of Images
Informal description
Let $f$ be a function defined on a set $t$ in a preordered type, and suppose $f$ is antitone on $t$. If $a$ is a lower bound for $t$ and $a \in t$, then $f(a)$ is an upper bound for the image $f(t)$.
AntitoneOn.mem_lowerBounds_image theorem
(Hf : AntitoneOn f t) (Hst : s ⊆ t) : a ∈ upperBounds s → a ∈ t → f a ∈ lowerBounds (f '' s)
Full source 
theorem mem_lowerBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) :
    a ∈ upperBounds s → a ∈ t → f a ∈ lowerBounds (f '' s) :=
  Hf.dual_right.mem_upperBounds_image Hst
Antitone Functions Map Upper Bounds to Lower Bounds of Images
Informal description
Let $f$ be a function defined on a set $t$ in a preordered type $\alpha$, and let $s$ be a subset of $t$. If $f$ is antitone on $t$, $a$ is an upper bound for $s$, and $a \in t$, then $f(a)$ is a lower bound for the image $f(s)$.
AntitoneOn.mem_lowerBounds_image_self theorem
(Hf : AntitoneOn f t) : a ∈ upperBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)
Full source 
theorem mem_lowerBounds_image_self (Hf : AntitoneOn f t) :
    a ∈ upperBounds t → a ∈ t → f a ∈ lowerBounds (f '' t) :=
  Hf.dual_right.mem_upperBounds_image_self
Antitone Functions Map Upper Bounds to Lower Bounds of Their Own Image
Informal description
Let $f$ be a function defined on a set $t$ in a preordered type, and suppose $f$ is antitone on $t$. If $a$ is an upper bound for $t$ and $a \in t$, then $f(a)$ is a lower bound for the image $f(t)$.
AntitoneOn.image_lowerBounds_subset_upperBounds_image theorem
(Hf : AntitoneOn f t) (Hst : s ⊆ t) : f '' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s)
Full source 
theorem image_lowerBounds_subset_upperBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) :
    f '' (lowerBounds s ∩ t)f '' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s) :=
  Hf.dual_right.image_lowerBounds_subset_lowerBounds_image Hst
Antitone Functions Map Lower Bounds to Upper Bounds of Images
Informal description
Let $f$ be a function defined on a set $t$ in a partially ordered type, and let $s$ be a subset of $t$. If $f$ is antitone on $t$, then the image under $f$ of the intersection of $t$ with the lower bounds of $s$ is contained in the set of upper bounds of the image $f(s)$. In other words, for any $a \in t$ that is a lower bound for $s$, $f(a)$ is an upper bound for $f(s)$.
AntitoneOn.image_upperBounds_subset_lowerBounds_image theorem
(Hf : AntitoneOn f t) (Hst : s ⊆ t) : f '' (upperBounds s ∩ t) ⊆ lowerBounds (f '' s)
Full source 
theorem image_upperBounds_subset_lowerBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) :
    f '' (upperBounds s ∩ t)f '' (upperBounds s ∩ t) ⊆ lowerBounds (f '' s) :=
  Hf.dual_right.image_upperBounds_subset_upperBounds_image Hst
Antitone Functions Map Upper Bounds to Lower Bounds of Images
Informal description
Let $f$ be a function defined on a set $t$ in a partially ordered type, and let $s$ be a subset of $t$. If $f$ is antitone on $t$, then the image under $f$ of the intersection of $t$ with the upper bounds of $s$ is contained in the set of lower bounds of the image $f(s)$. In other words, for any $a \in t$ that is an upper bound for $s$, $f(a)$ is a lower bound for $f(s)$.
AntitoneOn.map_bddAbove theorem
(Hf : AntitoneOn f t) (Hst : s ⊆ t) : (upperBounds s ∩ t).Nonempty → BddBelow (f '' s)
Full source 
/-- The image under an antitone function of a set which is bounded above is bounded below. -/
theorem map_bddAbove (Hf : AntitoneOn f t) (Hst : s ⊆ t) :
    (upperBoundsupperBounds s ∩ t).Nonempty → BddBelow (f '' s) :=
  Hf.dual_right.map_bddAbove Hst
Antitone Functions Map Bounded-Above Sets to Bounded-Below Images
Informal description
Let $f$ be a function defined on a set $t$ in a partially ordered type, and let $s$ be a subset of $t$. If $f$ is antitone on $t$ and there exists an upper bound of $s$ that belongs to $t$, then the image $f(s)$ is bounded below.
AntitoneOn.map_bddBelow theorem
(Hf : AntitoneOn f t) (Hst : s ⊆ t) : (lowerBounds s ∩ t).Nonempty → BddAbove (f '' s)
Full source 
/-- The image under an antitone function of a set which is bounded below is bounded above. -/
theorem map_bddBelow (Hf : AntitoneOn f t) (Hst : s ⊆ t) :
    (lowerBoundslowerBounds s ∩ t).Nonempty → BddAbove (f '' s) :=
  Hf.dual_right.map_bddBelow Hst
Antitone functions map bounded-below sets to bounded-above sets
Informal description
Let $f$ be a function defined on a set $t$ in a partially ordered type, and let $s$ be a subset of $t$. If $f$ is antitone on $t$ and there exists a lower bound of $s$ that belongs to $t$, then the image $f(s)$ is bounded above.
AntitoneOn.map_isGreatest theorem
(Hf : AntitoneOn f t) : IsGreatest t a → IsLeast (f '' t) (f a)
Full source 
/-- An antitone map sends a greatest element of a set to a least element of its image. -/
theorem map_isGreatest (Hf : AntitoneOn f t) : IsGreatest t a → IsLeast (f '' t) (f a) :=
  Hf.dual_right.map_isGreatest
Antitone Function Maps Greatest Elements to Least Elements
Informal description
Let $f$ be an antitone function defined on a set $t$ in a partially ordered type. If $a$ is the greatest element of $t$, then $f(a)$ is the least element of the image $f(t)$.
AntitoneOn.map_isLeast theorem
(Hf : AntitoneOn f t) : IsLeast t a → IsGreatest (f '' t) (f a)
Full source 
/-- An antitone map sends a least element of a set to a greatest element of its image. -/
theorem map_isLeast (Hf : AntitoneOn f t) : IsLeast t a → IsGreatest (f '' t) (f a) :=
  Hf.dual_right.map_isLeast
Antitone Function Maps Least Elements to Greatest Elements
Informal description
Let $f$ be a function defined on a set $t$ in a partially ordered type, and suppose $f$ is antitone on $t$. If $a$ is the least element of $t$, then $f(a)$ is the greatest element of the image $f(t)$.
Monotone.mem_upperBounds_image theorem
(Ha : a ∈ upperBounds s) : f a ∈ upperBounds (f '' s)
Full source 
theorem mem_upperBounds_image (Ha : a ∈ upperBounds s) : f a ∈ upperBounds (f '' s) :=
  forall_mem_image.2 fun _ H => Hf (Ha H)
Monotone Function Preserves Upper Bounds
Informal description
Let $f$ be a monotone function on a set $s$ in a preordered type $\alpha$, and let $a$ be an upper bound of $s$. Then $f(a)$ is an upper bound of the image $f(s)$.
Monotone.mem_lowerBounds_image theorem
(Ha : a ∈ lowerBounds s) : f a ∈ lowerBounds (f '' s)
Full source 
theorem mem_lowerBounds_image (Ha : a ∈ lowerBounds s) : f a ∈ lowerBounds (f '' s) :=
  forall_mem_image.2 fun _ H => Hf (Ha H)
Monotone functions preserve lower bounds under images
Informal description
Let $f : \alpha \to \beta$ be a monotone function between partially ordered types, and let $s \subseteq \alpha$. If $a \in \alpha$ is a lower bound for $s$ (i.e., $a \leq x$ for all $x \in s$), then $f(a)$ is a lower bound for the image $f(s)$ (i.e., $f(a) \leq y$ for all $y \in f(s)$).
Monotone.image_upperBounds_subset_upperBounds_image theorem
: f '' upperBounds s ⊆ upperBounds (f '' s)
Full source 
theorem image_upperBounds_subset_upperBounds_image :
    f '' upperBounds sf '' upperBounds s ⊆ upperBounds (f '' s) := by
  rintro _ ⟨a, ha, rfl⟩
  exact Hf.mem_upperBounds_image ha
Monotone Image of Upper Bounds is Contained in Upper Bounds of Image
Informal description
Let $f : \alpha \to \beta$ be a monotone function between preordered types, and let $s$ be a subset of $\alpha$. Then the image under $f$ of the set of upper bounds of $s$ is contained in the set of upper bounds of the image $f(s)$. In other words, for any upper bound $a$ of $s$, $f(a)$ is an upper bound of $f(s)$.
Monotone.image_lowerBounds_subset_lowerBounds_image theorem
: f '' lowerBounds s ⊆ lowerBounds (f '' s)
Full source 
theorem image_lowerBounds_subset_lowerBounds_image : f '' lowerBounds sf '' lowerBounds s ⊆ lowerBounds (f '' s) :=
  Hf.dual.image_upperBounds_subset_upperBounds_image
Monotone Image of Lower Bounds is Contained in Lower Bounds of Image
Informal description
Let $f : \alpha \to \beta$ be a monotone function between preordered types, and let $s$ be a subset of $\alpha$. Then the image under $f$ of the set of lower bounds of $s$ is contained in the set of lower bounds of the image $f(s)$. In other words, for any lower bound $a$ of $s$, $f(a)$ is a lower bound of $f(s)$.
Monotone.map_bddAbove theorem
: BddAbove s → BddAbove (f '' s)
Full source 
/-- The image under a monotone function of a set which is bounded above is bounded above. See also
`BddAbove.image2`. -/
theorem map_bddAbove : BddAbove s → BddAbove (f '' s)
  | ⟨C, hC⟩ => ⟨f C, Hf.mem_upperBounds_image hC⟩
Monotone Functions Preserve Upper Bounds on Images
Informal description
Let $f : \alpha \to \beta$ be a monotone function between partially ordered types, and let $s \subseteq \alpha$ be a set that is bounded above. Then the image $f(s)$ is also bounded above.
Monotone.map_bddBelow theorem
: BddBelow s → BddBelow (f '' s)
Full source 
/-- The image under a monotone function of a set which is bounded below is bounded below. See also
`BddBelow.image2`. -/
theorem map_bddBelow : BddBelow s → BddBelow (f '' s)
  | ⟨C, hC⟩ => ⟨f C, Hf.mem_lowerBounds_image hC⟩
Monotone Functions Preserve Lower Bounds on Images
Informal description
Let $f : \alpha \to \beta$ be a monotone function between partially ordered types, and let $s \subseteq \alpha$ be a set that is bounded below. Then the image $f(s)$ is also bounded below.
Monotone.map_isLeast theorem
(Ha : IsLeast s a) : IsLeast (f '' s) (f a)
Full source 
/-- A monotone map sends a least element of a set to a least element of its image. -/
theorem map_isLeast (Ha : IsLeast s a) : IsLeast (f '' s) (f a) :=
  ⟨mem_image_of_mem _ Ha.1, Hf.mem_lowerBounds_image Ha.2⟩
Monotone Functions Preserve Least Elements Under Images
Informal description
Let $f : \alpha \to \beta$ be a monotone function between partially ordered types, and let $s \subseteq \alpha$. If $a \in \alpha$ is a least element of $s$ (i.e., $a \in s$ and $a \leq x$ for all $x \in s$), then $f(a)$ is a least element of the image $f(s)$ (i.e., $f(a) \in f(s)$ and $f(a) \leq y$ for all $y \in f(s)$).
Monotone.map_isGreatest theorem
(Ha : IsGreatest s a) : IsGreatest (f '' s) (f a)
Full source 
/-- A monotone map sends a greatest element of a set to a greatest element of its image. -/
theorem map_isGreatest (Ha : IsGreatest s a) : IsGreatest (f '' s) (f a) :=
  ⟨mem_image_of_mem _ Ha.1, Hf.mem_upperBounds_image Ha.2⟩
Monotone Functions Preserve Greatest Elements Under Images
Informal description
Let $f : \alpha \to \beta$ be a monotone function between partially ordered types, and let $s \subseteq \alpha$. If $a \in \alpha$ is a greatest element of $s$ (i.e., $a \in s$ and $x \leq a$ for all $x \in s$), then $f(a)$ is a greatest element of the image $f(s)$ (i.e., $f(a) \in f(s)$ and $y \leq f(a)$ for all $y \in f(s)$).
Antitone.mem_upperBounds_image theorem
: a ∈ lowerBounds s → f a ∈ upperBounds (f '' s)
Full source 
theorem mem_upperBounds_image : a ∈ lowerBounds s → f a ∈ upperBounds (f '' s) :=
  hf.dual_right.mem_lowerBounds_image
Antitone Functions Map Lower Bounds to Upper Bounds of Image
Informal description
Let $f : \alpha \to \beta$ be an antitone function between preordered types, and let $s \subseteq \alpha$. If $a \in \alpha$ is a lower bound for $s$ (i.e., $a \leq x$ for all $x \in s$), then $f(a)$ is an upper bound for the image $f(s)$ (i.e., $y \leq f(a)$ for all $y \in f(s)$).
Antitone.mem_lowerBounds_image theorem
: a ∈ upperBounds s → f a ∈ lowerBounds (f '' s)
Full source 
theorem mem_lowerBounds_image : a ∈ upperBounds s → f a ∈ lowerBounds (f '' s) :=
  hf.dual_right.mem_upperBounds_image
Antitone Functions Map Upper Bounds to Lower Bounds of Image
Informal description
Let $f : \alpha \to \beta$ be an antitone function between preordered types, and let $s \subseteq \alpha$. If $a \in \alpha$ is an upper bound of $s$ (i.e., $x \leq a$ for all $x \in s$), then $f(a)$ is a lower bound of the image $f(s)$ (i.e., $f(a) \leq y$ for all $y \in f(s)$).
Antitone.image_lowerBounds_subset_upperBounds_image theorem
: f '' lowerBounds s ⊆ upperBounds (f '' s)
Full source 
theorem image_lowerBounds_subset_upperBounds_image : f '' lowerBounds sf '' lowerBounds s ⊆ upperBounds (f '' s) :=
  hf.dual_right.image_lowerBounds_subset_lowerBounds_image
Antitone Functions Map Lower Bounds to Upper Bounds of Image
Informal description
Let $f : \alpha \to \beta$ be an antitone function between preordered types, and let $s$ be a subset of $\alpha$. Then the image under $f$ of the set of lower bounds of $s$ is contained in the set of upper bounds of the image $f(s)$. In other words, for any lower bound $a$ of $s$, $f(a)$ is an upper bound of $f(s)$.
Antitone.image_upperBounds_subset_lowerBounds_image theorem
: f '' upperBounds s ⊆ lowerBounds (f '' s)
Full source 
theorem image_upperBounds_subset_lowerBounds_image : f '' upperBounds sf '' upperBounds s ⊆ lowerBounds (f '' s) :=
  hf.dual_right.image_upperBounds_subset_upperBounds_image
Antitone Functions Map Upper Bounds to Lower Bounds of Image
Informal description
Let $f : \alpha \to \beta$ be an antitone function between preordered types, and let $s$ be a subset of $\alpha$. Then the image under $f$ of the set of upper bounds of $s$ is contained in the set of lower bounds of the image $f(s)$. In other words, for any upper bound $a$ of $s$, $f(a)$ is a lower bound of $f(s)$.
Antitone.map_bddAbove theorem
: BddAbove s → BddBelow (f '' s)
Full source 
/-- The image under an antitone function of a set which is bounded above is bounded below. -/
theorem map_bddAbove : BddAbove s → BddBelow (f '' s) :=
  hf.dual_right.map_bddAbove
Antitone Functions Map Bounded Above Sets to Bounded Below Sets
Informal description
Let $f : \alpha \to \beta$ be an antitone function between partially ordered types, and let $s \subseteq \alpha$ be a set that is bounded above. Then the image $f(s)$ is bounded below.
Antitone.map_bddBelow theorem
: BddBelow s → BddAbove (f '' s)
Full source 
/-- The image under an antitone function of a set which is bounded below is bounded above. -/
theorem map_bddBelow : BddBelow s → BddAbove (f '' s) :=
  hf.dual_right.map_bddBelow
Antitone Functions Map Bounded Below Sets to Bounded Above Sets
Informal description
Let $f : \alpha \to \beta$ be an antitone function between partially ordered types, and let $s \subseteq \alpha$ be a set that is bounded below. Then the image $f(s)$ is bounded above.
Antitone.map_isGreatest theorem
: IsGreatest s a → IsLeast (f '' s) (f a)
Full source 
/-- An antitone map sends a greatest element of a set to a least element of its image. -/
theorem map_isGreatest : IsGreatest s a → IsLeast (f '' s) (f a) :=
  hf.dual_right.map_isGreatest
Antitone Functions Map Greatest Elements to Least Elements Under Images
Informal description
Let $f : \alpha \to \beta$ be an antitone function between partially ordered types, and let $s \subseteq \alpha$. If $a$ is a greatest element of $s$ (i.e., $a \in s$ and $x \leq a$ for all $x \in s$), then $f(a)$ is a least element of the image $f(s)$ (i.e., $f(a) \in f(s)$ and $f(a) \leq y$ for all $y \in f(s)$).
Antitone.map_isLeast theorem
: IsLeast s a → IsGreatest (f '' s) (f a)
Full source 
/-- An antitone map sends a least element of a set to a greatest element of its image. -/
theorem map_isLeast : IsLeast s a → IsGreatest (f '' s) (f a) :=
  hf.dual_right.map_isLeast
Antitone Functions Map Least Elements to Greatest Elements Under Images
Informal description
Let $f : \alpha \to \beta$ be an antitone function between partially ordered types, and let $s \subseteq \alpha$. If $a \in \alpha$ is a least element of $s$ (i.e., $a \in s$ and $a \leq x$ for all $x \in s$), then $f(a)$ is a greatest element of the image $f(s)$ (i.e., $f(a) \in f(s)$ and $y \leq f(a)$ for all $y \in f(s)$).
StrictMono.mem_upperBounds_image theorem
(hf : StrictMono f) : f a ∈ upperBounds (f '' s) ↔ a ∈ upperBounds s
Full source 
lemma StrictMono.mem_upperBounds_image (hf : StrictMono f) :
    f a ∈ upperBounds (f '' s)f a ∈ upperBounds (f '' s) ↔ a ∈ upperBounds s := by simp [upperBounds, hf.le_iff_le]
Strictly Monotone Function Preserves Upper Bounds Under Image
Informal description
Let $f$ be a strictly monotone function. For any element $a$ and set $s$, the image $f(a)$ is an upper bound of the image set $f(s)$ if and only if $a$ is an upper bound of $s$.
StrictMono.mem_lowerBounds_image theorem
(hf : StrictMono f) : f a ∈ lowerBounds (f '' s) ↔ a ∈ lowerBounds s
Full source 
lemma StrictMono.mem_lowerBounds_image (hf : StrictMono f) :
    f a ∈ lowerBounds (f '' s)f a ∈ lowerBounds (f '' s) ↔ a ∈ lowerBounds s :=  by simp [lowerBounds, hf.le_iff_le]
Strictly Monotone Function Preserves Lower Bounds Under Images
Informal description
Let \( f \) be a strictly monotone function. Then for any element \( a \) and set \( s \), the image \( f(a) \) is a lower bound of the image set \( f(s) \) if and only if \( a \) is a lower bound of \( s \).
StrictMono.map_isLeast theorem
(hf : StrictMono f) : IsLeast (f '' s) (f a) ↔ IsLeast s a
Full source 
lemma StrictMono.map_isLeast (hf : StrictMono f) : IsLeastIsLeast (f '' s) (f a) ↔ IsLeast s a := by
  simp [IsLeast, hf.injective.eq_iff, hf.mem_lowerBounds_image]
Strictly Monotone Function Preserves Least Elements Under Image
Informal description
Let $f$ be a strictly monotone function between partially ordered types. For any element $a$ and set $s$, the image $f(a)$ is the least element of the image set $f(s)$ if and only if $a$ is the least element of $s$.
StrictMono.map_isGreatest theorem
(hf : StrictMono f) : IsGreatest (f '' s) (f a) ↔ IsGreatest s a
Full source 
lemma StrictMono.map_isGreatest (hf : StrictMono f) :
    IsGreatestIsGreatest (f '' s) (f a) ↔ IsGreatest s a := by
  simp [IsGreatest, hf.injective.eq_iff, hf.mem_upperBounds_image]
Strictly Monotone Function Preserves Greatest Elements Under Image
Informal description
Let $f$ be a strictly monotone function between partially ordered types. For any element $a$ and set $s$, the image $f(a)$ is the greatest element of the image set $f(s)$ if and only if $a$ is the greatest element of $s$.
StrictAnti.mem_upperBounds_image theorem
(hf : StrictAnti f) : f a ∈ upperBounds (f '' s) ↔ a ∈ lowerBounds s
Full source 
lemma StrictAnti.mem_upperBounds_image (hf : StrictAnti f) :
    f a ∈ upperBounds (f '' s)f a ∈ upperBounds (f '' s) ↔ a ∈ lowerBounds s := by
  simp [upperBounds, lowerBounds, hf.le_iff_le]
Strictly Antitone Function Preserves Bounds: $f(a)$ is upper bound of $f(s)$ iff $a$ is lower bound of $s$
Informal description
Let $f$ be a strictly antitone function between partially ordered types. For any element $a$ and set $s$ in the domain, the image $f(a)$ is an upper bound of the image set $f(s)$ if and only if $a$ is a lower bound of $s$.
StrictAnti.mem_lowerBounds_image theorem
(hf : StrictAnti f) : f a ∈ lowerBounds (f '' s) ↔ a ∈ upperBounds s
Full source 
lemma StrictAnti.mem_lowerBounds_image (hf : StrictAnti f) :
    f a ∈ lowerBounds (f '' s)f a ∈ lowerBounds (f '' s) ↔ a ∈ upperBounds s := by
  simp [upperBounds, lowerBounds, hf.le_iff_le]
Strictly antitone function preserves upper/lower bounds in images: $f(a) \in \text{lowerBounds}(f(s)) \leftrightarrow a \in \text{upperBounds}(s)$
Informal description
Let $f$ be a strictly antitone function. Then for any element $a$ and set $s$, the image $f(a)$ is a lower bound of the image set $f(s)$ if and only if $a$ is an upper bound of $s$.
StrictAnti.map_isLeast theorem
(hf : StrictAnti f) : IsLeast (f '' s) (f a) ↔ IsGreatest s a
Full source 
lemma StrictAnti.map_isLeast (hf : StrictAnti f) : IsLeastIsLeast (f '' s) (f a) ↔ IsGreatest s a := by
  simp [IsLeast, IsGreatest, hf.injective.eq_iff, hf.mem_lowerBounds_image]
Strictly Antitone Function Maps Greatest Elements to Least Elements: $f(a) = \min f(s) \iff a = \max s$
Informal description
Let $f$ be a strictly antitone function between partially ordered types. For any element $a$ and set $s$ in the domain, the image $f(a)$ is the least element of the image set $f(s)$ if and only if $a$ is the greatest element of $s$.
StrictAnti.map_isGreatest theorem
(hf : StrictAnti f) : IsGreatest (f '' s) (f a) ↔ IsLeast s a
Full source 
lemma StrictAnti.map_isGreatest (hf : StrictAnti f) : IsGreatestIsGreatest (f '' s) (f a) ↔ IsLeast s a := by
  simp [IsLeast, IsGreatest, hf.injective.eq_iff, hf.mem_upperBounds_image]
Strictly Antitone Function Maps Greatest Elements to Least Elements: $f(a) = \max f(s) \iff a = \min s$
Informal description
Let $f$ be a strictly antitone function between partially ordered types. For any element $a$ and set $s$ in the domain, the image $f(a)$ is the greatest element of the image set $f(s)$ if and only if $a$ is the least element of $s$.
mem_upperBounds_image2 theorem
(ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (image2 f s t)
Full source 
theorem mem_upperBounds_image2 (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) :
    f a b ∈ upperBounds (image2 f s t) :=
  forall_mem_image2.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy
Upper Bound Preservation under Binary Operation
Informal description
Let $s$ and $t$ be sets in types with preorders, and let $f$ be a function. If $a$ is an upper bound for $s$ and $b$ is an upper bound for $t$, then $f(a,b)$ is an upper bound for the set $\{f(x,y) \mid x \in s, y \in t\}$.
mem_lowerBounds_image2 theorem
(ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (image2 f s t)
Full source 
theorem mem_lowerBounds_image2 (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) :
    f a b ∈ lowerBounds (image2 f s t) :=
  forall_mem_image2.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy
Lower bound preservation under binary function application
Informal description
Let $s$ and $t$ be sets in a partially ordered type, and let $f$ be a function. If $a$ is a lower bound of $s$ and $b$ is a lower bound of $t$, then $f(a,b)$ is a lower bound of the image of $s \times t$ under $f$.
image2_upperBounds_upperBounds_subset theorem
: image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t)
Full source 
theorem image2_upperBounds_upperBounds_subset :
    image2image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t) :=
  image2_subset_iff.2 fun _ ha _ hb ↦ mem_upperBounds_image2 h₀ h₁ ha hb
Inclusion of Upper Bounds under Binary Function Application
Informal description
For any binary function $f$ and sets $s$ and $t$ in a partially ordered type, the image of the product of the upper bounds of $s$ and the upper bounds of $t$ under $f$ is contained in the set of upper bounds of the image of $s \times t$ under $f$. In other words, \[ f(\text{upperBounds}(s), \text{upperBounds}(t)) \subseteq \text{upperBounds}(f(s, t)). \]
image2_lowerBounds_lowerBounds_subset theorem
: image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t)
Full source 
theorem image2_lowerBounds_lowerBounds_subset :
    image2image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t) :=
  image2_subset_iff.2 fun _ ha _ hb ↦ mem_lowerBounds_image2 h₀ h₁ ha hb
Inclusion of Lower Bounds under Binary Function Application
Informal description
For any binary function $f$ and sets $s$ and $t$ in a partially ordered type, the image of the product of the lower bounds of $s$ and the lower bounds of $t$ under $f$ is contained in the set of lower bounds of the image of $s \times t$ under $f$. In other words, \[ f(\text{lowerBounds}(s), \text{lowerBounds}(t)) \subseteq \text{lowerBounds}(f(s, t)). \]
BddAbove.image2 theorem
: BddAbove s → BddAbove t → BddAbove (image2 f s t)
Full source 
/-- See also `Monotone.map_bddAbove`. -/
protected theorem BddAbove.image2 :
    BddAbove s → BddAbove t → BddAbove (image2 f s t) := by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_upperBounds_image2 h₀ h₁ ha hb⟩
Binary Image of Bounded Above Sets is Bounded Above
Informal description
If sets $s$ and $t$ in a partially ordered type are bounded above, then their image under a binary function $f$, denoted as $\{f(x,y) \mid x \in s, y \in t\}$, is also bounded above.
BddBelow.image2 theorem
: BddBelow s → BddBelow t → BddBelow (image2 f s t)
Full source 
/-- See also `Monotone.map_bddBelow`. -/
protected theorem BddBelow.image2 :
    BddBelow s → BddBelow t → BddBelow (image2 f s t) := by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_lowerBounds_image2 h₀ h₁ ha hb⟩
Binary Image of Bounded Below Sets is Bounded Below
Informal description
If sets $s$ and $t$ in a partially ordered type are bounded below, then their image under a binary function $f$, denoted as $\text{image2}\,f\,s\,t$, is also bounded below.
IsGreatest.image2 theorem
(ha : IsGreatest s a) (hb : IsGreatest t b) : IsGreatest (image2 f s t) (f a b)
Full source 
protected theorem IsGreatest.image2 (ha : IsGreatest s a) (hb : IsGreatest t b) :
    IsGreatest (image2 f s t) (f a b) :=
  ⟨mem_image2_of_mem ha.1 hb.1, mem_upperBounds_image2 h₀ h₁ ha.2 hb.2⟩
Greatest Element Preservation under Binary Operation: $f(\max s, \max t) = \max f(s,t)$
Informal description
Let $s$ and $t$ be sets in a partially ordered type, and let $f$ be a function. If $a$ is the greatest element of $s$ and $b$ is the greatest element of $t$, then $f(a,b)$ is the greatest element of the set $\{f(x,y) \mid x \in s, y \in t\}$.
IsLeast.image2 theorem
(ha : IsLeast s a) (hb : IsLeast t b) : IsLeast (image2 f s t) (f a b)
Full source 
protected theorem IsLeast.image2 (ha : IsLeast s a) (hb : IsLeast t b) :
    IsLeast (image2 f s t) (f a b) :=
  ⟨mem_image2_of_mem ha.1 hb.1, mem_lowerBounds_image2 h₀ h₁ ha.2 hb.2⟩
Least Element Preservation under Binary Operation: $f(\min s, \min t) = \min f(s,t)$
Informal description
Let $s$ and $t$ be sets in partially ordered types, and let $f$ be a binary function. If $a$ is the least element of $s$ and $b$ is the least element of $t$, then $f(a,b)$ is the least element of the set $\{f(x,y) \mid x \in s, y \in t\}$.
mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds theorem
(ha : a ∈ upperBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (image2 f s t)
Full source 
theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds (ha : a ∈ upperBounds s)
    (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (image2 f s t) :=
  forall_mem_image2.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy
Upper Bound Preservation under Function Application: $f(\text{upperBounds}(s), \text{lowerBounds}(t)) \subseteq \text{upperBounds}(f(s,t))$
Informal description
Let $s$ and $t$ be sets in types with preorders, and let $f$ be a function. If $a$ is an upper bound of $s$ and $b$ is a lower bound of $t$, then $f(a,b)$ is an upper bound of the image of $s \times t$ under $f$, i.e., $f(a,b) \in \text{upperBounds}(f(s,t))$.
mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds theorem
(ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (image2 f s t)
Full source 
theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds (ha : a ∈ lowerBounds s)
    (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (image2 f s t) :=
  forall_mem_image2.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy
Lower bound of image under function of lower and upper bounds
Informal description
Let $s$ be a set in a partially ordered type $\alpha$ and $t$ a set in a partially ordered type $\beta$. If $a$ is a lower bound of $s$ and $b$ is an upper bound of $t$, then for any function $f : \alpha \to \beta \to \gamma$, the value $f(a,b)$ is a lower bound of the image set $\{f(x,y) \mid x \in s, y \in t\}$.
image2_upperBounds_lowerBounds_subset_upperBounds_image2 theorem
: image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t)
Full source 
theorem image2_upperBounds_lowerBounds_subset_upperBounds_image2 :
    image2image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t) :=
  image2_subset_iff.2 fun _ ha _ hb ↦
    mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb
Upper Bound Preservation under Function Application: $f(\text{upperBounds}(s), \text{lowerBounds}(t)) \subseteq \text{upperBounds}(f(s,t))$
Informal description
For any function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the image of the product of upper bounds of $s$ and lower bounds of $t$ under $f$ is contained in the set of upper bounds of the image of $s \times t$ under $f$. In other words, \[ f(\text{upperBounds}(s), \text{lowerBounds}(t)) \subseteq \text{upperBounds}(f(s,t)). \]
image2_lowerBounds_upperBounds_subset_lowerBounds_image2 theorem
: image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t)
Full source 
theorem image2_lowerBounds_upperBounds_subset_lowerBounds_image2 :
    image2image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t) :=
  image2_subset_iff.2 fun _ ha _ hb ↦
    mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha hb
Lower Bound Preservation under Function Application: $f(\text{lowerBounds}(s), \text{upperBounds}(t)) \subseteq \text{lowerBounds}(f(s,t))$
Informal description
For any function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the image of the product of lower bounds of $s$ and upper bounds of $t$ under $f$ is contained in the set of lower bounds of the image of $s \times t$ under $f$. In other words, \[ f(\text{lowerBounds}(s), \text{upperBounds}(t)) \subseteq \text{lowerBounds}(f(s,t)). \]
BddAbove.bddAbove_image2_of_bddBelow theorem
: BddAbove s → BddBelow t → BddAbove (Set.image2 f s t)
Full source 
theorem BddAbove.bddAbove_image2_of_bddBelow :
    BddAbove s → BddBelow t → BddAbove (Set.image2 f s t) := by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩
Image of Bounded Above and Below Sets under a Function is Bounded Above
Informal description
If a set $s$ is bounded above and a set $t$ is bounded below, then the image of $s \times t$ under a function $f$ is bounded above.
BddBelow.bddBelow_image2_of_bddAbove theorem
: BddBelow s → BddAbove t → BddBelow (Set.image2 f s t)
Full source 
theorem BddBelow.bddBelow_image2_of_bddAbove :
    BddBelow s → BddAbove t → BddBelow (Set.image2 f s t) := by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha hb⟩
Image of Bounded Below and Above Sets under a Function is Bounded Below
Informal description
If a set $s$ is bounded below and a set $t$ is bounded above, then the image of $s \times t$ under a function $f$ is bounded below.
IsGreatest.isGreatest_image2_of_isLeast theorem
(ha : IsGreatest s a) (hb : IsLeast t b) : IsGreatest (Set.image2 f s t) (f a b)
Full source 
theorem IsGreatest.isGreatest_image2_of_isLeast (ha : IsGreatest s a) (hb : IsLeast t b) :
    IsGreatest (Set.image2 f s t) (f a b) :=
  ⟨mem_image2_of_mem ha.1 hb.1,
    mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha.2 hb.2⟩
Greatest Element of Image under Function of Greatest and Least Elements
Informal description
Let $s$ be a set in a partially ordered type $\alpha$ with greatest element $a$, and let $t$ be a set in a partially ordered type $\beta$ with least element $b$. Then for any function $f : \alpha \to \beta \to \gamma$, the value $f(a,b)$ is the greatest element of the image set $\{f(x,y) \mid x \in s, y \in t\}$.
IsLeast.isLeast_image2_of_isGreatest theorem
(ha : IsLeast s a) (hb : IsGreatest t b) : IsLeast (Set.image2 f s t) (f a b)
Full source 
theorem IsLeast.isLeast_image2_of_isGreatest (ha : IsLeast s a) (hb : IsGreatest t b) :
    IsLeast (Set.image2 f s t) (f a b) :=
  ⟨mem_image2_of_mem ha.1 hb.1,
    mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha.2 hb.2⟩
Least Element of Image under Function of Least and Greatest Elements
Informal description
Let $s$ be a set in a partially ordered type $\alpha$ and $t$ a set in a partially ordered type $\beta$. If $a$ is the least element of $s$ and $b$ is the greatest element of $t$, then for any function $f : \alpha \to \beta \to \gamma$, the value $f(a,b)$ is the least element of the image set $\{f(x,y) \mid x \in s, y \in t\}$.
mem_upperBounds_image2_of_mem_lowerBounds theorem
(ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (image2 f s t)
Full source 
theorem mem_upperBounds_image2_of_mem_lowerBounds (ha : a ∈ lowerBounds s)
    (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (image2 f s t) :=
  forall_mem_image2.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy
Upper Bound of Image from Lower Bounds
Informal description
Let $s$ and $t$ be sets in a partially ordered type $\alpha$, and let $f : \alpha \to \alpha \to \alpha$ be a function. If $a$ is a lower bound of $s$ and $b$ is a lower bound of $t$, then $f(a, b)$ is an upper bound of the image of $f$ on $s \times t$, i.e., $f(a, b) \in \text{upperBounds}(f(s, t))$.
mem_lowerBounds_image2_of_mem_upperBounds theorem
(ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (image2 f s t)
Full source 
theorem mem_lowerBounds_image2_of_mem_upperBounds (ha : a ∈ upperBounds s)
    (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (image2 f s t) :=
  forall_mem_image2.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy
Lower Bound of Image under Function of Upper Bounds
Informal description
Let $s$ and $t$ be sets in a partially ordered type $\alpha$, and let $f : \alpha \to \alpha \to \alpha$ be a function. If $a$ is an upper bound of $s$ and $b$ is an upper bound of $t$, then $f(a, b)$ is a lower bound of the set $\{f(x, y) \mid x \in s, y \in t\}$.
image2_upperBounds_upperBounds_subset_upperBounds_image2 theorem
: image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t)
Full source 
theorem image2_upperBounds_upperBounds_subset_upperBounds_image2 :
    image2image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t) :=
  image2_subset_iff.2 fun _ ha _ hb ↦
    mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb
Image of Lower Bounds under Function is Subset of Upper Bounds of Image
Informal description
Let $s$ and $t$ be sets in a partially ordered type $\alpha$, and let $f : \alpha \to \alpha \to \alpha$ be a function. The image of the lower bounds of $s$ and $t$ under $f$ is contained in the upper bounds of the image of $s$ and $t$ under $f$, i.e., $$ f(\text{lowerBounds}(s), \text{lowerBounds}(t)) \subseteq \text{upperBounds}(f(s, t)). $$
image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 theorem
: image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t)
Full source 
theorem image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 :
    image2image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t) :=
  image2_subset_iff.2 fun _ ha _ hb ↦
    mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha hb
Image of Upper Bounds under Function is Subset of Lower Bounds of Image
Informal description
Let $s$ and $t$ be sets in a partially ordered type $\alpha$, and let $f : \alpha \to \alpha \to \alpha$ be a function. The image of the upper bounds of $s$ and $t$ under $f$ is contained in the lower bounds of the image of $s$ and $t$ under $f$, i.e., $$ f(\text{upperBounds}(s), \text{upperBounds}(t)) \subseteq \text{lowerBounds}(f(s, t)). $$
BddBelow.image2_bddAbove theorem
: BddBelow s → BddBelow t → BddAbove (Set.image2 f s t)
Full source 
theorem BddBelow.image2_bddAbove : BddBelow s → BddBelow t → BddAbove (Set.image2 f s t) := by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb⟩
Bounded Below Sets Imply Bounded Above Image under Binary Function
Informal description
Let $s$ and $t$ be sets in a partially ordered type $\alpha$, and let $f : \alpha \to \alpha \to \alpha$ be a function. If $s$ is bounded below and $t$ is bounded below, then the image $\{f(x, y) \mid x \in s, y \in t\}$ is bounded above.
BddAbove.image2_bddBelow theorem
: BddAbove s → BddAbove t → BddBelow (Set.image2 f s t)
Full source 
theorem BddAbove.image2_bddBelow : BddAbove s → BddAbove t → BddBelow (Set.image2 f s t) := by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha hb⟩
Bounded Above Sets Imply Bounded Below Image under Binary Function
Informal description
Let $s$ and $t$ be sets in a partially ordered type $\alpha$, and let $f : \alpha \to \alpha \to \alpha$ be a function. If $s$ is bounded above and $t$ is bounded above, then the image $\{f(x, y) \mid x \in s, y \in t\}$ is bounded below.
IsLeast.isGreatest_image2 theorem
(ha : IsLeast s a) (hb : IsLeast t b) : IsGreatest (Set.image2 f s t) (f a b)
Full source 
theorem IsLeast.isGreatest_image2 (ha : IsLeast s a) (hb : IsLeast t b) :
    IsGreatest (Set.image2 f s t) (f a b) :=
  ⟨mem_image2_of_mem ha.1 hb.1, mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha.2 hb.2⟩
Greatest Element of Image under Least Elements
Informal description
Let $s$ and $t$ be sets in a partially ordered type $\alpha$, and let $f : \alpha \to \alpha \to \alpha$ be a function. If $a$ is the least element of $s$ and $b$ is the least element of $t$, then $f(a, b)$ is the greatest element of the image of $f$ on $s \times t$.
IsGreatest.isLeast_image2 theorem
(ha : IsGreatest s a) (hb : IsGreatest t b) : IsLeast (Set.image2 f s t) (f a b)
Full source 
theorem IsGreatest.isLeast_image2 (ha : IsGreatest s a) (hb : IsGreatest t b) :
    IsLeast (Set.image2 f s t) (f a b) :=
  ⟨mem_image2_of_mem ha.1 hb.1, mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha.2 hb.2⟩
Least Element of Image under Greatest Elements
Informal description
Let $s$ and $t$ be sets in a partially ordered type $\alpha$, and let $f : \alpha \to \alpha \to \alpha$ be a function. If $a$ is the greatest element of $s$ and $b$ is the greatest element of $t$, then $f(a, b)$ is the least element of the image set $\{f(x, y) \mid x \in s, y \in t\}$.
mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds theorem
(ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (image2 f s t)
Full source 
theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds (ha : a ∈ lowerBounds s)
    (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (image2 f s t) :=
  forall_mem_image2.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy
Upper Bound Preservation under Image2 with Mixed Bounds
Informal description
Let $s$ be a set in a partially ordered type $\alpha$ and $t$ a set in a partially ordered type $\beta$. If $a$ is a lower bound of $s$ and $b$ is an upper bound of $t$, then for any function $f : \alpha \to \beta \to \gamma$, the element $f(a,b)$ is an upper bound of the image set $\operatorname{image2} f s t$.
mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds theorem
(ha : a ∈ upperBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (image2 f s t)
Full source 
theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds (ha : a ∈ upperBounds s)
    (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (image2 f s t) :=
  forall_mem_image2.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy
Lower Bound Preservation under Function Application on Bounded Sets
Informal description
Let $s$ and $t$ be sets in types with preorders, and let $f$ be a function. If $a$ is an upper bound of $s$ and $b$ is a lower bound of $t$, then $f(a,b)$ is a lower bound of the image of $f$ on $s \times t$ (i.e., $f(a,b) \in \text{lowerBounds}(f(s,t))$).
image2_lowerBounds_upperBounds_subset_upperBounds_image2 theorem
: image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t)
Full source 
theorem image2_lowerBounds_upperBounds_subset_upperBounds_image2 :
    image2image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t) :=
  image2_subset_iff.2 fun _ ha _ hb ↦
    mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb
Upper Bound Preservation under Image2 with Lower and Upper Bounds
Informal description
Let $s$ be a set in a partially ordered type $\alpha$ and $t$ a set in a partially ordered type $\beta$. For any function $f : \alpha \to \beta \to \gamma$, the image of the lower bounds of $s$ and the upper bounds of $t$ under $f$ is contained in the set of upper bounds of the image of $s$ and $t$ under $f$. In other words, $$ f(\text{lowerBounds}(s), \text{upperBounds}(t)) \subseteq \text{upperBounds}(f(s, t)). $$
image2_upperBounds_lowerBounds_subset_lowerBounds_image2 theorem
: image2 f (upperBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t)
Full source 
theorem image2_upperBounds_lowerBounds_subset_lowerBounds_image2 :
    image2image2 f (upperBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t) :=
  image2_subset_iff.2 fun _ ha _ hb ↦
    mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha hb
Inclusion of Function Image of Bounds in Lower Bounds of Function Image
Informal description
Let $f$ be a function, $s$ a set with upper bounds, and $t$ a set with lower bounds. Then the image of the upper bounds of $s$ and the lower bounds of $t$ under $f$ is contained in the set of lower bounds of the image of $s$ and $t$ under $f$. In other words, $$ f(\text{upperBounds}(s), \text{lowerBounds}(t)) \subseteq \text{lowerBounds}(f(s, t)). $$
BddBelow.bddAbove_image2_of_bddAbove theorem
: BddBelow s → BddAbove t → BddAbove (Set.image2 f s t)
Full source 
theorem BddBelow.bddAbove_image2_of_bddAbove :
    BddBelow s → BddAbove t → BddAbove (Set.image2 f s t) := by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb⟩
Bounded Below and Above Sets Imply Bounded Above Image Set
Informal description
If a set $s$ in a partially ordered type is bounded below and a set $t$ in a partially ordered type is bounded above, then the image set $\operatorname{image2} f s t$ is bounded above.
BddAbove.bddBelow_image2_of_bddAbove theorem
: BddAbove s → BddBelow t → BddBelow (Set.image2 f s t)
Full source 
theorem BddAbove.bddBelow_image2_of_bddAbove :
    BddAbove s → BddBelow t → BddBelow (Set.image2 f s t) := by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩
Bounded Above and Below Sets Imply Bounded Below Image Set
Informal description
If a set $s$ in a partially ordered type is bounded above and a set $t$ in a partially ordered type is bounded below, then the image set $\operatorname{image2} f s t$ is bounded below.
IsLeast.isGreatest_image2_of_isGreatest theorem
(ha : IsLeast s a) (hb : IsGreatest t b) : IsGreatest (Set.image2 f s t) (f a b)
Full source 
theorem IsLeast.isGreatest_image2_of_isGreatest (ha : IsLeast s a) (hb : IsGreatest t b) :
    IsGreatest (Set.image2 f s t) (f a b) :=
  ⟨mem_image2_of_mem ha.1 hb.1,
    mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha.2 hb.2⟩
Greatest Element of Image under Function with Least and Greatest Inputs
Informal description
Let $s$ be a set in a partially ordered type $\alpha$ and $t$ a set in a partially ordered type $\beta$. If $a$ is the least element of $s$ and $b$ is the greatest element of $t$, then $f(a,b)$ is the greatest element of the image set $\operatorname{image2} f s t$.
IsGreatest.isLeast_image2_of_isLeast theorem
(ha : IsGreatest s a) (hb : IsLeast t b) : IsLeast (Set.image2 f s t) (f a b)
Full source 
theorem IsGreatest.isLeast_image2_of_isLeast (ha : IsGreatest s a) (hb : IsLeast t b) :
    IsLeast (Set.image2 f s t) (f a b) :=
  ⟨mem_image2_of_mem ha.1 hb.1,
    mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha.2 hb.2⟩
Least Element of Image under Function with Greatest and Least Inputs
Informal description
Let $s$ be a set in a partially ordered type $\alpha$ and $t$ a set in a partially ordered type $\beta$. If $a$ is the greatest element of $s$ and $b$ is the least element of $t$, then $f(a,b)$ is the least element of the image of $f$ on $s \times t$.
bddAbove_prod theorem
{s : Set (α × β)} : BddAbove s ↔ BddAbove (Prod.fst '' s) ∧ BddAbove (Prod.snd '' s)
Full source 
lemma bddAbove_prod {s : Set (α × β)} :
    BddAboveBddAbove s ↔ BddAbove (Prod.fst '' s) ∧ BddAbove (Prod.snd '' s) :=
  ⟨fun ⟨p, hp⟩ ↦ ⟨⟨p.1, forall_mem_image.2 fun _q hq ↦ (hp hq).1⟩,
    ⟨p.2, forall_mem_image.2 fun _q hq ↦ (hp hq).2⟩⟩,
    fun ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ ↦ ⟨⟨x, y⟩, fun _p hp ↦
      ⟨hx <| mem_image_of_mem _ hp, hy <| mem_image_of_mem _ hp⟩⟩⟩
Boundedness of Product Set via Componentwise Boundedness
Informal description
For any set $s$ of pairs in $\alpha \times \beta$, $s$ is bounded above if and only if the projection of $s$ onto the first component is bounded above in $\alpha$ and the projection of $s$ onto the second component is bounded above in $\beta$.
bddBelow_prod theorem
{s : Set (α × β)} : BddBelow s ↔ BddBelow (Prod.fst '' s) ∧ BddBelow (Prod.snd '' s)
Full source 
lemma bddBelow_prod {s : Set (α × β)} :
    BddBelowBddBelow s ↔ BddBelow (Prod.fst '' s) ∧ BddBelow (Prod.snd '' s) :=
  bddAbove_prod (α := αᵒᵈ) (β := βᵒᵈ)
Boundedness Below of Product Set via Componentwise Boundedness Below
Informal description
For any set $s$ of pairs in $\alpha \times \beta$, $s$ is bounded below if and only if the projection of $s$ onto the first component is bounded below in $\alpha$ and the projection of $s$ onto the second component is bounded below in $\beta$.
bddAbove_range_prod theorem
{F : ι → α × β} : BddAbove (range F) ↔ BddAbove (range <| Prod.fst ∘ F) ∧ BddAbove (range <| Prod.snd ∘ F)
Full source 
lemma bddAbove_range_prod {F : ι → α × β} :
    BddAboveBddAbove (range F) ↔ BddAbove (range <| Prod.fst ∘ F) ∧ BddAbove (range <| Prod.snd ∘ F) := by
  simp only [bddAbove_prod, ← range_comp]
Boundedness of Range of Product-Valued Function via Componentwise Boundedness
Informal description
For any function $F$ from an index set $\iota$ to the product space $\alpha \times \beta$, the range of $F$ is bounded above if and only if the range of the first component function $\text{Prod.fst} \circ F$ is bounded above in $\alpha$ and the range of the second component function $\text{Prod.snd} \circ F$ is bounded above in $\beta$.
bddBelow_range_prod theorem
{F : ι → α × β} : BddBelow (range F) ↔ BddBelow (range <| Prod.fst ∘ F) ∧ BddBelow (range <| Prod.snd ∘ F)
Full source 
lemma bddBelow_range_prod {F : ι → α × β} :
    BddBelowBddBelow (range F) ↔ BddBelow (range <| Prod.fst ∘ F) ∧ BddBelow (range <| Prod.snd ∘ F) :=
  bddAbove_range_prod (α := αᵒᵈ) (β := βᵒᵈ)
Boundedness Below of Range of Product-Valued Function via Componentwise Boundedness Below
Informal description
For any function $F$ from an index set $\iota$ to the product space $\alpha \times \beta$, the range of $F$ is bounded below if and only if the range of the first component function $\pi_1 \circ F$ is bounded below in $\alpha$ and the range of the second component function $\pi_2 \circ F$ is bounded below in $\beta$.
isLUB_prod theorem
{s : Set (α × β)} (p : α × β) : IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
Full source 
theorem isLUB_prod {s : Set (α × β)} (p : α × β) :
    IsLUBIsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2 := by
  refine
    ⟨fun H =>
      ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩,
        ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩,
      fun H => ⟨?_, ?_⟩⟩
  · suffices h : (a, p.2)(a, p.2) ∈ upperBounds s from (H.2 h).1
    exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩
  · suffices h : (p.1, a)(p.1, a) ∈ upperBounds s from (H.2 h).2
    exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩
  · exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩
  · exact fun q hq =>
      ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq,
        H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩
Least Upper Bound in Product Space via Componentwise Least Upper Bounds
Informal description
For any set $s \subseteq \alpha \times \beta$ and any point $p = (p_1, p_2) \in \alpha \times \beta$, $p$ is the least upper bound of $s$ if and only if $p_1$ is the least upper bound of the projection of $s$ onto $\alpha$ (i.e., $\text{Prod.fst} \ '' \ s$) and $p_2$ is the least upper bound of the projection of $s$ onto $\beta$ (i.e., $\text{Prod.snd} \ '' \ s$).
isGLB_prod theorem
{s : Set (α × β)} (p : α × β) : IsGLB s p ↔ IsGLB (Prod.fst '' s) p.1 ∧ IsGLB (Prod.snd '' s) p.2
Full source 
theorem isGLB_prod {s : Set (α × β)} (p : α × β) :
    IsGLBIsGLB s p ↔ IsGLB (Prod.fst '' s) p.1 ∧ IsGLB (Prod.snd '' s) p.2 :=
  @isLUB_prod αᵒᵈ βᵒᵈ _ _ _ _
Greatest Lower Bound in Product Space via Componentwise Greatest Lower Bounds
Informal description
For any set $s \subseteq \alpha \times \beta$ and any point $p = (p_1, p_2) \in \alpha \times \beta$, $p$ is the greatest lower bound of $s$ if and only if $p_1$ is the greatest lower bound of the projection of $s$ onto $\alpha$ (i.e., $\pi_1(s)$) and $p_2$ is the greatest lower bound of the projection of $s$ onto $\beta$ (i.e., $\pi_2(s)$).
bddAbove_pi theorem
{s : Set (∀ a, π a)} : BddAbove s ↔ ∀ a, BddAbove (Function.eval a '' s)
Full source 
lemma bddAbove_pi {s : Set (∀ a, π a)} :
    BddAboveBddAbove s ↔ ∀ a, BddAbove (Function.eval a '' s) :=
  ⟨fun ⟨f, hf⟩ a ↦ ⟨f a, forall_mem_image.2 fun _ hg ↦ hf hg a⟩,
    fun h ↦ ⟨fun a ↦ (h a).some, fun _ hg a ↦ (h a).some_mem <| mem_image_of_mem _ hg⟩⟩
Boundedness of Function Set in Product Space via Pointwise Boundedness
Informal description
For a set $s$ of functions in a product space $\prod_{a} \pi_a$, $s$ is bounded above if and only if for every index $a$, the set of evaluations $\{f(a) \mid f \in s\}$ is bounded above.
bddBelow_pi theorem
{s : Set (∀ a, π a)} : BddBelow s ↔ ∀ a, BddBelow (Function.eval a '' s)
Full source 
lemma bddBelow_pi {s : Set (∀ a, π a)} :
    BddBelowBddBelow s ↔ ∀ a, BddBelow (Function.eval a '' s) :=
  bddAbove_pi (π := fun a ↦ (π a)ᵒᵈ)
Boundedness Below of Function Set in Product Space via Pointwise Boundedness Below
Informal description
For a set $s$ of functions in a product space $\prod_{a} \pi_a$, $s$ is bounded below if and only if for every index $a$, the set of evaluations $\{f(a) \mid f \in s\}$ is bounded below.
bddAbove_range_pi theorem
{F : ι → ∀ a, π a} : BddAbove (range F) ↔ ∀ a, BddAbove (range fun i ↦ F i a)
Full source 
lemma bddAbove_range_pi {F : ι → ∀ a, π a} :
    BddAboveBddAbove (range F) ↔ ∀ a, BddAbove (range fun i ↦ F i a) := by
  simp only [bddAbove_pi, ← range_comp]
  rfl
Boundedness of Range of Family of Functions in Product Space
Informal description
For a family of functions $F : \iota \to \prod_{a} \pi_a$, the range of $F$ is bounded above if and only if for each index $a$, the range of the evaluations $(F_i a)_{i \in \iota}$ is bounded above.
bddBelow_range_pi theorem
{F : ι → ∀ a, π a} : BddBelow (range F) ↔ ∀ a, BddBelow (range fun i ↦ F i a)
Full source 
lemma bddBelow_range_pi {F : ι → ∀ a, π a} :
    BddBelowBddBelow (range F) ↔ ∀ a, BddBelow (range fun i ↦ F i a) :=
  bddAbove_range_pi (π := fun a ↦ (π a)ᵒᵈ)
Boundedness Below of Range of Family of Functions in Product Space via Componentwise Boundedness Below
Informal description
For a family of functions $F : \iota \to \prod_{a} \pi_a$, the range of $F$ is bounded below if and only if for each index $a$, the range of the evaluations $(F_i a)_{i \in \iota}$ is bounded below.
isLUB_pi theorem
{s : Set (∀ a, π a)} {f : ∀ a, π a} : IsLUB s f ↔ ∀ a, IsLUB (Function.eval a '' s) (f a)
Full source 
theorem isLUB_pi {s : Set (∀ a, π a)} {f : ∀ a, π a} :
    IsLUBIsLUB s f ↔ ∀ a, IsLUB (Function.eval a '' s) (f a) := by
  classical
    refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩
    · suffices h : Function.updateFunction.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
      exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
    · exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
    · exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)
Least Upper Bound in Product Space via Componentwise Evaluation
Informal description
For a set $s$ of functions in a product space $\prod_{a} \pi_a$ and a function $f \in \prod_{a} \pi_a$, $f$ is the least upper bound of $s$ if and only if for every index $a$, the evaluation $f(a)$ is the least upper bound of the set of evaluations $\{g(a) \mid g \in s\}$.
isGLB_pi theorem
{s : Set (∀ a, π a)} {f : ∀ a, π a} : IsGLB s f ↔ ∀ a, IsGLB (Function.eval a '' s) (f a)
Full source 
theorem isGLB_pi {s : Set (∀ a, π a)} {f : ∀ a, π a} :
    IsGLBIsGLB s f ↔ ∀ a, IsGLB (Function.eval a '' s) (f a) :=
  @isLUB_pi α (fun a => (π a)ᵒᵈ) _ s f
Greatest Lower Bound in Product Space via Componentwise Evaluation
Informal description
For a set $s$ of functions in a product space $\prod_{a} \pi_a$ and a function $f \in \prod_{a} \pi_a$, $f$ is the greatest lower bound of $s$ if and only if for every index $a$, the evaluation $f(a)$ is the greatest lower bound of the set of evaluations $\{g(a) \mid g \in s\}$.
IsGLB.of_image theorem
[Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y}, f x ≤ f y ↔ x ≤ y) {s : Set α} {x : α} (hx : IsGLB (f '' s) (f x)) : IsGLB s x
Full source 
theorem IsGLB.of_image [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y}, f x ≤ f y ↔ x ≤ y)
    {s : Set α} {x : α} (hx : IsGLB (f '' s) (f x)) : IsGLB s x :=
  ⟨fun _ hy => hf.1 <| hx.1 <| mem_image_of_mem _ hy, fun _ hy =>
    hf.1 <| hx.2 <| Monotone.mem_lowerBounds_image (fun _ _ => hf.2) hy⟩
Greatest Lower Bound Preservation under Order-Reflecting Function
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $f : \alpha \to \beta$ be a function such that for all $x, y \in \alpha$, $f(x) \leq f(y)$ if and only if $x \leq y$. If $f(x)$ is the greatest lower bound of the image $f(s)$ of a set $s \subseteq \alpha$, then $x$ is the greatest lower bound of $s$.
IsLUB.of_image theorem
[Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y}, f x ≤ f y ↔ x ≤ y) {s : Set α} {x : α} (hx : IsLUB (f '' s) (f x)) : IsLUB s x
Full source 
theorem IsLUB.of_image [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y}, f x ≤ f y ↔ x ≤ y)
    {s : Set α} {x : α} (hx : IsLUB (f '' s) (f x)) : IsLUB s x :=
  ⟨fun _ hy => hf.1 <| hx.1 <| mem_image_of_mem _ hy, fun _ hy =>
    hf.1 <| hx.2 <| Monotone.mem_upperBounds_image (fun _ _ => hf.2) hy⟩
Least Upper Bound Preservation under Order-Reflecting Function
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $f : \alpha \to \beta$ be a function such that for all $x, y \in \alpha$, $f(x) \leq f(y)$ if and only if $x \leq y$. If $f(x)$ is the least upper bound of the image $f(s)$ of a set $s \subseteq \alpha$, then $x$ is the least upper bound of $s$.
BddAbove.range_mono theorem
[Preorder β] {f : α → β} (g : α → β) (h : ∀ a, f a ≤ g a) (hbdd : BddAbove (range g)) : BddAbove (range f)
Full source 
lemma BddAbove.range_mono [Preorder β] {f : α → β} (g : α → β) (h : ∀ a, f a ≤ g a)
    (hbdd : BddAbove (range g)) : BddAbove (range f) := by
  obtain ⟨C, hC⟩ := hbdd
  use C
  rintro - ⟨x, rfl⟩
  exact (h x).trans (hC <| mem_range_self x)
Boundedness of Range under Pointwise Inequality
Informal description
Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder. Given two functions $f, g : \alpha \to \beta$ such that $f(a) \leq g(a)$ for all $a \in \alpha$, if the range of $g$ is bounded above in $\beta$, then the range of $f$ is also bounded above in $\beta$.
BddBelow.range_mono theorem
[Preorder β] (f : α → β) {g : α → β} (h : ∀ a, f a ≤ g a) (hbdd : BddBelow (range f)) : BddBelow (range g)
Full source 
lemma BddBelow.range_mono [Preorder β] (f : α → β) {g : α → β} (h : ∀ a, f a ≤ g a)
    (hbdd : BddBelow (range f)) : BddBelow (range g) :=
  BddAbove.range_mono (β := βᵒᵈ) f h hbdd
Lower Boundedness of Range under Pointwise Inequality
Informal description
Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder. Given two functions $f, g \colon \alpha \to \beta$ such that $f(a) \leq g(a)$ for all $a \in \alpha$, if the range of $f$ is bounded below in $\beta$, then the range of $g$ is also bounded below in $\beta$.
BddAbove.range_comp theorem
{γ : Type*} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ} (hf : BddAbove (range f)) (hg : Monotone g) : BddAbove (range (fun x => g (f x)))
Full source 
lemma BddAbove.range_comp {γ : Type*} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ}
    (hf : BddAbove (range f)) (hg : Monotone g) : BddAbove (range (fun x => g (f x))) := by
  change BddAbove (range (g ∘ f))
  simpa only [Set.range_comp] using hg.map_bddAbove hf
Monotone Composition Preserves Upper Boundedness of Range
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be types with preorders on $\beta$ and $\gamma$. Given a function $f \colon \alpha \to \beta$ whose range is bounded above and a monotone function $g \colon \beta \to \gamma$, the range of the composition $g \circ f$ is also bounded above.
BddBelow.range_comp theorem
{γ : Type*} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ} (hf : BddBelow (range f)) (hg : Monotone g) : BddBelow (range (fun x => g (f x)))
Full source 
lemma BddBelow.range_comp {γ : Type*} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ}
    (hf : BddBelow (range f)) (hg : Monotone g) : BddBelow (range (fun x => g (f x))) := by
  change BddBelow (range (g ∘ f))
  simpa only [Set.range_comp] using hg.map_bddBelow hf
Monotone Composition Preserves Lower Boundedness of Range
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be types with preorders on $\beta$ and $\gamma$. Given a function $f \colon \alpha \to \beta$ whose range is bounded below and a monotone function $g \colon \beta \to \gamma$, the range of the composition $g \circ f$ is also bounded below.