feat(order/bounds): Image under an order_iso and upper_bounds commute (#9555)

Author: YaelDillies

src/order/bounds.lean

@@ -769,6 +769,17 @@ lemma mem_lower_bounds_image (Ha : a ∈ lower_bounds s) :
   f a ∈ lower_bounds (f '' s) :=
 ball_image_of_ball (assume x H, Hf (Ha ‹x ∈ s›))
 
+lemma image_upper_bounds_subset_upper_bounds_image (hf : monotone f) :
+  f '' upper_bounds s ⊆ upper_bounds (f '' s) :=
+begin
+  rintro _ ⟨a, ha, rfl⟩,
+  exact hf.mem_upper_bounds_image ha,
+end
+
+lemma image_lower_bounds_subset_lower_bounds_image (hf : monotone f) :
+  f '' lower_bounds s ⊆ lower_bounds (f '' s) :=
+@image_upper_bounds_subset_upper_bounds_image (order_dual α) (order_dual β) _ _ _ _ hf.dual
+
 /-- The image under a monotone function of a set which is bounded above is bounded above. -/
 lemma map_bdd_above (hf : monotone f) : bdd_above s → bdd_above (f '' s)
 | ⟨C, hC⟩ := ⟨f C, hf.mem_upper_bounds_image hC⟩
@@ -842,38 +853,48 @@ lemma is_glb_prod [preorder α] [preorder β] {s : set (α × β)} (p : α × β
 
 namespace order_iso
 
-variables [preorder α] [preorder β]
+variables [preorder α] [preorder β] (f : α ≃o β)
+
+lemma upper_bounds_image {s : set α} :
+  upper_bounds (f '' s) = f '' upper_bounds s :=
+subset.antisymm
+  (λ x hx, ⟨f.symm x, λ y hy, f.le_symm_apply.2 (hx $ mem_image_of_mem _ hy), f.apply_symm_apply x⟩)
+  f.monotone.image_upper_bounds_subset_upper_bounds_image
+
+lemma lower_bounds_image {s : set α} :
+  lower_bounds (f '' s) = f '' lower_bounds s :=
+@upper_bounds_image (order_dual α) (order_dual β) _ _ f.dual _
 
-@[simp] lemma is_lub_image (f : α ≃o β) {s : set α} {x : β} :
+@[simp] lemma is_lub_image {s : set α} {x : β} :
   is_lub (f '' s) x ↔ is_lub s (f.symm x) :=
 ⟨λ h, is_lub.of_image (λ _ _, f.le_iff_le) ((f.apply_symm_apply x).symm ▸ h),
   λ h, is_lub.of_image (λ _ _, f.symm.le_iff_le) $ (f.symm_image_image s).symm ▸ h⟩
 
-lemma is_lub_image' (f : α ≃o β) {s : set α} {x : α} :
+lemma is_lub_image' {s : set α} {x : α} :
   is_lub (f '' s) (f x) ↔ is_lub s x :=
 by rw [is_lub_image, f.symm_apply_apply]
 
-@[simp] lemma is_glb_image (f : α ≃o β) {s : set α} {x : β} :
+@[simp] lemma is_glb_image {s : set α} {x : β} :
   is_glb (f '' s) x ↔ is_glb s (f.symm x) :=
 f.dual.is_lub_image
 
-lemma is_glb_image' (f : α ≃o β) {s : set α} {x : α} :
+lemma is_glb_image' {s : set α} {x : α} :
   is_glb (f '' s) (f x) ↔ is_glb s x :=
 f.dual.is_lub_image'
 
-@[simp] lemma is_lub_preimage (f : α ≃o β) {s : set β} {x : α} :
+@[simp] lemma is_lub_preimage {s : set β} {x : α} :
   is_lub (f ⁻¹' s) x ↔ is_lub s (f x) :=
 by rw [← f.symm_symm, ← image_eq_preimage, is_lub_image]
 
-lemma is_lub_preimage' (f : α ≃o β) {s : set β} {x : β} :
+lemma is_lub_preimage' {s : set β} {x : β} :
   is_lub (f ⁻¹' s) (f.symm x) ↔ is_lub s x :=
 by rw [is_lub_preimage, f.apply_symm_apply]
 
-@[simp] lemma is_glb_preimage (f : α ≃o β) {s : set β} {x : α} :
+@[simp] lemma is_glb_preimage {s : set β} {x : α} :
   is_glb (f ⁻¹' s) x ↔ is_glb s (f x) :=
 f.dual.is_lub_preimage
 
-lemma is_glb_preimage' (f : α ≃o β) {s : set β} {x : β} :
+lemma is_glb_preimage' {s : set β} {x : β} :
   is_glb (f ⁻¹' s) (f.symm x) ↔ is_glb s x :=
 f.dual.is_lub_preimage'
 

src/order/galois_connection.lean

@@ -224,14 +224,6 @@ namespace order_iso
 
 variables [preorder α] [preorder β]
 
-@[simp] lemma upper_bounds_image (e : α ≃o β) (s : set α) :
-  upper_bounds (e '' s) = e.symm ⁻¹' upper_bounds s :=
-e.to_galois_connection.upper_bounds_l_image s
-
-@[simp] lemma lower_bounds_image (e : α ≃o β) (s : set α) :
-  lower_bounds (e '' s) = e.symm ⁻¹' lower_bounds s :=
-e.dual.upper_bounds_image s
-
 @[simp] lemma bdd_above_image (e : α ≃o β) {s : set α} : bdd_above (e '' s) ↔ bdd_above s :=
 e.to_galois_connection.bdd_above_l_image