feat: add basic API lemmas for BddAbove (range f) and `BddBelow (ra…

…nge f)` (#9472)

This PR adds some basic API lemmas for `BddAbove (range f)` (resp `BddBelow`). This is a ubiquitous side condition when working with `iInf`/`iSup` in conditionally complete lattices, so I think it's worth having.



Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

Mathlib/Algebra/Bounds.lean

@@ -88,6 +88,16 @@ theorem IsLUB.inv (h : IsLUB s a) : IsGLB s⁻¹ a⁻¹ :=
 #align is_lub.inv IsLUB.inv
 #align is_lub.neg IsLUB.neg
 
+@[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
+
+@[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
+
 end InvNeg
 
 section mul_add
@@ -135,6 +145,17 @@ theorem BddBelow.mul {s t : Set M} (hs : BddBelow s) (ht : BddBelow t) : BddBelo
 #align bdd_below.mul BddBelow.mul
 #align bdd_below.add BddBelow.add
 
+@[to_additive]
+lemma BddAbove.range_mul {α : Type*} {f g : α → M} (hf : BddAbove (range f))
+    (hg : BddAbove (range g)) : BddAbove (range (fun x => f x * g x)) :=
+  BddAbove.range_comp (f := fun x => (⟨f x, g x⟩ : M × M))
+    (bddAbove_range_prod.mpr ⟨hf, hg⟩) (Monotone.mul' monotone_fst monotone_snd)
+
+@[to_additive]
+lemma BddBelow.range_mul {α : Type*} {f g : α → M} (hf : BddBelow (range f))
+    (hg : BddBelow (range g)) : BddBelow (range (fun x => f x * g x)) :=
+  BddAbove.range_mul (M := Mᵒᵈ) hf hg
+
 end mul_add
 
 section ConditionallyCompleteLattice
@@ -145,23 +166,23 @@ variable {ι G : Type*} [Group G] [ConditionallyCompleteLattice G]
   [CovariantClass G G (Function.swap (· * ·)) (· ≤ ·)] [Nonempty ι] {f : ι → G}
 
 @[to_additive]
-theorem ciSup_mul (hf : BddAbove (Set.range f)) (a : G) : (⨆ i, f i) * a = ⨆ i, f i * a :=
+theorem ciSup_mul (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) * a = ⨆ i, f i * a :=
   (OrderIso.mulRight a).map_ciSup hf
 #align csupr_mul ciSup_mul
 #align csupr_add ciSup_add
 
 @[to_additive]
-theorem ciSup_div (hf : BddAbove (Set.range f)) (a : G) : (⨆ i, f i) / a = ⨆ i, f i / a := by
+theorem ciSup_div (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) / a = ⨆ i, f i / a := by
   simp only [div_eq_mul_inv, ciSup_mul hf]
 #align csupr_div ciSup_div
 #align csupr_sub ciSup_sub
 
 @[to_additive]
-theorem ciInf_mul (hf : BddBelow (Set.range f)) (a : G) : (⨅ i, f i) * a = ⨅ i, f i * a :=
+theorem ciInf_mul (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) * a = ⨅ i, f i * a :=
   (OrderIso.mulRight a).map_ciInf hf
 
 @[to_additive]
-theorem ciInf_div (hf : BddBelow (Set.range f)) (a : G) : (⨅ i, f i) / a = ⨅ i, f i / a := by
+theorem ciInf_div (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) / a = ⨅ i, f i / a := by
   simp only [div_eq_mul_inv, ciInf_mul hf]
 
 end Right
@@ -172,13 +193,13 @@ variable {ι G : Type*} [Group G] [ConditionallyCompleteLattice G]
   [CovariantClass G G (· * ·) (· ≤ ·)] [Nonempty ι] {f : ι → G}
 
 @[to_additive]
-theorem mul_ciSup (hf : BddAbove (Set.range f)) (a : G) : (a * ⨆ i, f i) = ⨆ i, a * f i :=
+theorem mul_ciSup (hf : BddAbove (range f)) (a : G) : (a * ⨆ i, f i) = ⨆ i, a * f i :=
   (OrderIso.mulLeft a).map_ciSup hf
 #align mul_csupr mul_ciSup
 #align add_csupr add_ciSup
 
 @[to_additive]
-theorem mul_ciInf (hf : BddBelow (Set.range f)) (a : G) : (a * ⨅ i, f i) = ⨅ i, a * f i :=
+theorem mul_ciInf (hf : BddBelow (range f)) (a : G) : (a * ⨅ i, f i) = ⨅ i, a * f i :=
   (OrderIso.mulLeft a).map_ciInf hf
 
 end Left

Mathlib/Order/Bounds/Basic.lean

@@ -1662,6 +1662,27 @@ theorem IsLUB.of_image [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x
     hf.1 <| hx.2 <| Monotone.mem_upperBounds_image (fun _ _ => hf.2) hy⟩
 #align is_lub.of_image IsLUB.of_image
 
+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)
+
+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
+
+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
+
+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
+
 section ScottContinuous
 variable [Preorder α] [Preorder β] {f : α → β} {a : α}