Mathlib.Algebra.Order.Group.Pointwise.Bounds

mul_mem_upperBounds_mul theorem

(ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : a * b ∈ upperBounds (s * t)

Full source

@[to_additive]
lemma mul_mem_upperBounds_mul (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) :
    a * b ∈ upperBounds (s * t) := forall_mem_image2.2 fun _ hx _ hy => mul_le_mul' (ha hx) (hb hy)

Product of Upper Bounds is Upper Bound for Product Set

Informal description

Let $M$ be an ordered monoid, and let $s, t$ be subsets of $M$. If $a$ is an upper bound for $s$ and $b$ is an upper bound for $t$, then the product $a * b$ is an upper bound for the product set $s * t = \{x * y \mid x \in s, y \in t\}$.

subset_upperBounds_mul theorem

(s t : Set M) : upperBounds s * upperBounds t ⊆ upperBounds (s * t)

Full source

@[to_additive]
lemma subset_upperBounds_mul (s t : Set M) : upperBoundsupperBounds s * upperBounds t ⊆ upperBounds (s * t) :=
  image2_subset_iff.2 fun _ hx _ hy => mul_mem_upperBounds_mul hx hy

Product of Upper Bounds Subset Property in Ordered Monoids

Informal description

For any subsets $s$ and $t$ of an ordered monoid $M$, the product of their upper bounds is contained in the upper bounds of their product set, i.e., $\text{upperBounds}(s) \cdot \text{upperBounds}(t) \subseteq \text{upperBounds}(s \cdot t)$.

mul_mem_lowerBounds_mul theorem

(ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : a * b ∈ lowerBounds (s * t)

Full source

@[to_additive]
lemma mul_mem_lowerBounds_mul (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) :
    a * b ∈ lowerBounds (s * t) := mul_mem_upperBounds_mul (M := Mᵒᵈ) ha hb

Product of Lower Bounds is Lower Bound for Product Set

Informal description

Let $M$ be an ordered monoid, and let $s, t$ be subsets of $M$. If $a$ is a lower bound for $s$ and $b$ is a lower bound for $t$, then the product $a \cdot b$ is a lower bound for the product set $s \cdot t = \{x \cdot y \mid x \in s, y \in t\}$.

subset_lowerBounds_mul theorem

(s t : Set M) : lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t)

Full source

@[to_additive]
lemma subset_lowerBounds_mul (s t : Set M) : lowerBoundslowerBounds s * lowerBounds t ⊆ lowerBounds (s * t) :=
  subset_upperBounds_mul (M := Mᵒᵈ) _ _

Product of Lower Bounds Subset Property in Ordered Monoids

Informal description

For any subsets $s$ and $t$ of an ordered monoid $M$, the product of their lower bounds is contained in the lower bounds of their product set, i.e., $\text{lowerBounds}(s) \cdot \text{lowerBounds}(t) \subseteq \text{lowerBounds}(s \cdot t)$.

BddAbove.mul theorem

(hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t)

Full source

@[to_additive]
lemma BddAbove.mul (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t) :=
  (Nonempty.mul hs ht).mono (subset_upperBounds_mul s t)

Product of Bounded Above Sets is Bounded Above in Ordered Monoids

Informal description

If subsets $s$ and $t$ of an ordered monoid $M$ are bounded above, then their product set $s \cdot t = \{x \cdot y \mid x \in s, y \in t\}$ is also bounded above.

BddBelow.mul theorem

(hs : BddBelow s) (ht : BddBelow t) : BddBelow (s * t)

Full source

@[to_additive]
lemma BddBelow.mul (hs : BddBelow s) (ht : BddBelow t) : BddBelow (s * t) :=
  (Nonempty.mul hs ht).mono (subset_lowerBounds_mul s t)

Product of Bounded Below Sets is Bounded Below in Ordered Monoids

Informal description

For any subsets $s$ and $t$ of an ordered monoid $M$, if $s$ and $t$ are bounded below, then their product set $s \cdot t = \{x \cdot y \mid x \in s, y \in t\}$ is also bounded below.

BddAbove.range_mul theorem

(hf : BddAbove (range f)) (hg : BddAbove (range g)) : BddAbove (range fun i ↦ f i * g i)

Full source

@[to_additive]
lemma BddAbove.range_mul (hf : BddAbove (range f)) (hg : BddAbove (range g)) :
    BddAbove (range fun i ↦ f i * g i) :=
  .range_comp (f := fun i ↦ (f i, g i)) (bddAbove_range_prod.2 ⟨hf, hg⟩)
    (monotone_fst.mul' monotone_snd)

Product of Bounded Above Functions is Bounded Above

Informal description

Let $f$ and $g$ be functions such that their ranges are bounded above. Then the range of the function $i \mapsto f(i) \cdot g(i)$ is also bounded above.

BddBelow.range_mul theorem

(hf : BddBelow (range f)) (hg : BddBelow (range g)) : BddBelow (range fun i ↦ f i * g i)

Full source

@[to_additive]
lemma BddBelow.range_mul (hf : BddBelow (range f)) (hg : BddBelow (range g)) :
    BddBelow (range fun i ↦ f i * g i) := BddAbove.range_mul (M := Mᵒᵈ) hf hg

Product of Bounded Below Functions is Bounded Below

Informal description

Let $f$ and $g$ be functions such that their ranges are bounded below. Then the range of the function $i \mapsto f(i) \cdot g(i)$ is also bounded below.

bddAbove_inv theorem

: BddAbove s⁻¹ ↔ BddBelow s

Full source

@[to_additive (attr := simp)]
theorem bddAbove_inv : BddAboveBddAbove s⁻¹ ↔ BddBelow s :=
  (OrderIso.inv G).bddAbove_preimage

Inversion swaps upper and lower bounds: $s^{-1}$ bounded above iff $s$ bounded below

Informal description

For a set $s$ in an ordered group, the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is bounded above if and only if $s$ is bounded below.

bddBelow_inv theorem

: BddBelow s⁻¹ ↔ BddAbove s

Full source

@[to_additive (attr := simp)]
theorem bddBelow_inv : BddBelowBddBelow s⁻¹ ↔ BddAbove s :=
  (OrderIso.inv G).bddBelow_preimage

Inverse Set Bounded Below iff Original Set Bounded Above

Informal description

For a set $s$ in an ordered group, the set of inverses $s^{-1}$ is bounded below if and only if $s$ is bounded above.

BddAbove.inv theorem

(h : BddAbove s) : BddBelow s⁻¹

Full source

@[to_additive]
theorem BddAbove.inv (h : BddAbove s) : BddBelow s⁻¹ :=
  bddBelow_inv.2 h

Inversion Preserves Upper Bounds: $s$ bounded above implies $s^{-1}$ bounded below

Informal description

If a set $s$ in an ordered group is bounded above, then the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is bounded below.

BddBelow.inv theorem

(h : BddBelow s) : BddAbove s⁻¹

Full source

@[to_additive]
theorem BddBelow.inv (h : BddBelow s) : BddAbove s⁻¹ :=
  bddAbove_inv.2 h

Inversion Preserves Lower Boundedness to Upper Boundedness

Informal description

For any set $s$ in an ordered group, if $s$ is bounded below, then the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is bounded above.

isLUB_inv theorem

: IsLUB s⁻¹ a ↔ IsGLB s a⁻¹

Full source

@[to_additive (attr := simp)]
theorem isLUB_inv : IsLUBIsLUB s⁻¹ a ↔ IsGLB s a⁻¹ :=
  (OrderIso.inv G).isLUB_preimage

Least Upper Bound of Inverses Equals Greatest Lower Bound of Original Set's Inverses

Informal description

For a set $s$ in an ordered group and an element $a$, the set $s^{-1}$ has least upper bound $a$ if and only if $s$ has greatest lower bound $a^{-1}$.

isLUB_inv' theorem

: IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a

Full source

@[to_additive]
theorem isLUB_inv' : IsLUBIsLUB s⁻¹ a⁻¹ ↔ IsGLB s a :=
  (OrderIso.inv G).isLUB_preimage'

Least Upper Bound of Inverses Equals Greatest Lower Bound Inversion

Informal description

For a set $s$ in an ordered group and an element $a$, the set $s^{-1}$ has least upper bound $a^{-1}$ if and only if $s$ has greatest lower bound $a$.

IsGLB.inv theorem

(h : IsGLB s a) : IsLUB s⁻¹ a⁻¹

Full source

@[to_additive]
theorem IsGLB.inv (h : IsGLB s a) : IsLUB s⁻¹ a⁻¹ :=
  isLUB_inv'.2 h

Inversion of Greatest Lower Bound Yields Least Upper Bound of Inverses

Informal description

If $a$ is the greatest lower bound of a set $s$ in an ordered group, then $a^{-1}$ is the least upper bound of the set of inverses $s^{-1}$.

isGLB_inv theorem

: IsGLB s⁻¹ a ↔ IsLUB s a⁻¹

Full source

@[to_additive (attr := simp)]
theorem isGLB_inv : IsGLBIsGLB s⁻¹ a ↔ IsLUB s a⁻¹ :=
  (OrderIso.inv G).isGLB_preimage

Inversion Reverses Bounds: $\text{IsGLB}(s^{-1}, a) \leftrightarrow \text{IsLUB}(s, a^{-1})$

Informal description

For a set $s$ in an ordered group and an element $a$, the set of inverses $s^{-1}$ has greatest lower bound $a$ if and only if the set $s$ has least upper bound $a^{-1}$.

isGLB_inv' theorem

: IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a

Full source

@[to_additive]
theorem isGLB_inv' : IsGLBIsGLB s⁻¹ a⁻¹ ↔ IsLUB s a :=
  (OrderIso.inv G).isGLB_preimage'

Characterization of Greatest Lower Bound of Inverses via Least Upper Bound

Informal description

For a set $s$ in an ordered group and an element $a$, the element $a^{-1}$ is the greatest lower bound of the set $s^{-1}$ (the set of inverses of elements in $s$) if and only if $a$ is the least upper bound of $s$.

IsLUB.inv theorem

(h : IsLUB s a) : IsGLB s⁻¹ a⁻¹

Full source

@[to_additive]
theorem IsLUB.inv (h : IsLUB s a) : IsGLB s⁻¹ a⁻¹ :=
  isGLB_inv'.2 h

Inversion Preserves Bounds: Least Upper Bound Implies Greatest Lower Bound of Inverses

Informal description

Let $s$ be a subset of an ordered group and $a$ an element. If $a$ is the least upper bound of $s$, then $a^{-1}$ is the greatest lower bound of the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$.

BddBelow.range_inv theorem

{α : Type*} {f : α → G} (hf : BddBelow (range f)) : BddAbove (range (fun x => (f x)⁻¹))

Full source

@[to_additive]
lemma BddBelow.range_inv {α : Type*} {f : α → G} (hf : BddBelow (range f)) :
    BddAbove (range (fun x => (f x)⁻¹)) :=
  hf.range_comp (OrderIso.inv G).monotone

Inverse of a Bounded Below Function is Bounded Above

Informal description

Let $G$ be an ordered group, $\alpha$ a type, and $f : \alpha \to G$ a function. If the range of $f$ is bounded below, then the range of the function $\lambda x, (f x)^{-1}$ is bounded above.

BddAbove.range_inv theorem

{α : Type*} {f : α → G} (hf : BddAbove (range f)) : BddBelow (range (fun x => (f x)⁻¹))

Full source

@[to_additive]
lemma BddAbove.range_inv {α : Type*} {f : α → G} (hf : BddAbove (range f)) :
    BddBelow (range (fun x => (f x)⁻¹)) :=
  BddBelow.range_inv (G := Gᵒᵈ) hf

Inverse of a Bounded Above Function is Bounded Below

Informal description

Let $G$ be an ordered group, $\alpha$ a type, and $f : \alpha \to G$ a function. If the range of $f$ is bounded above, then the range of the function $\lambda x, (f x)^{-1}$ is bounded below.