feat(order/bounds): add is_lub_pi and is_glb_pi (#8521)

src/order/basic.lean

@@ -415,6 +415,10 @@ instance pi.preorder {ι : Type u} {α : ι → Type v} [∀ i, preorder (α i)]
   le_refl  := λ a i, le_refl (a i),
   le_trans := λ a b c h₁ h₂ i, le_trans (h₁ i) (h₂ i) }
 
+lemma function.monotone_eval {ι : Type u} {α : ι → Type v} [∀ i, preorder (α i)] (i : ι) :
+  monotone (function.eval i : (Π i, α i) → α i) :=
+λ f g H, H i
+
 lemma pi.le_def {ι : Type u} {α : ι → Type v} [∀ i, preorder (α i)] {x y : Π i, α i} :
   x ≤ y ↔ ∀ i, x i ≤ y i :=
 iff.rfl

src/order/bounds.lean

@@ -725,6 +725,17 @@ h.exists_between' h₂ $ sub_lt_self _ hε
 
 end linear_ordered_add_comm_group
 
+lemma is_lub_pi {π : α → Type*} [Π a, preorder (π a)] (s : set (Π a, π a)) (f : Π a, π a)
+  (hs : ∀ a, is_lub (function.eval a '' s) (f a)) :
+  is_lub s f :=
+⟨λ g hg a, (hs a).1 (mem_image_of_mem _ hg),
+  λ g hg a, (hs a).2 $ λ y ⟨g', hg', hy⟩, hy ▸ hg hg' a⟩
+
+lemma is_glb_pi {π : α → Type*} [Π a, preorder (π a)] (s : set (Π a, π a)) (f : Π a, π a)
+  (hs : ∀ a, is_glb (function.eval a '' s) (f a)) :
+  is_glb s f :=
+@is_lub_pi α (λ a, order_dual (π a)) _ s f hs
+
 /-!
 ### Images of upper/lower bounds under monotone functions
 -/