From 3f4b83689aa7c670d4647e3844af47fff143f2fd Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 3 Aug 2021 11:13:40 +0000
Subject: [PATCH] feat(order/bounds): add `is_lub_pi` and `is_glb_pi` (#8521)

---
 src/order/basic.lean  |  4 ++++
 src/order/bounds.lean | 11 +++++++++++
 2 files changed, 15 insertions(+)

diff --git a/src/order/basic.lean b/src/order/basic.lean
index aab452458023f..b2f6472aca922 100644
--- a/src/order/basic.lean
+++ b/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
diff --git a/src/order/bounds.lean b/src/order/bounds.lean
index 25a98d0afb2aa..34b39d1249926 100644
--- a/src/order/bounds.lean
+++ b/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
 -/