From 96d5730674a0ef313b7aa03994a16e330e7f6d1a Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Thu, 22 Apr 2021 10:34:39 +0000
Subject: [PATCH] feat(topology/continuous_function): lemmas about pointwise
 sup/inf (#7249)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
---
 src/data/finset/lattice.lean                | 10 ++++--
 src/topology/continuous_function/basic.lean | 36 +++++++++++++++++++++
 2 files changed, 43 insertions(+), 3 deletions(-)

diff --git a/src/data/finset/lattice.lean b/src/data/finset/lattice.lean
index 5016b689514af..324f5662e7f8e 100644
--- a/src/data/finset/lattice.lean
+++ b/src/data/finset/lattice.lean
@@ -457,6 +457,7 @@ end inf
 section sup
 variables {C : β → Type*} [Π (b : β), semilattice_sup_bot (C b)]
 
+@[simp]
 protected lemma sup_apply (s : finset α) (f : α → Π (b : β), C b) (b : β) :
   s.sup f b = s.sup (λ a, f a b) :=
 comp_sup_eq_sup_comp (λ x : Π b : β, C b, x b) (λ i j, rfl) rfl
@@ -466,6 +467,7 @@ end sup
 section inf
 variables {C : β → Type*} [Π (b : β), semilattice_inf_top (C b)]
 
+@[simp]
 protected lemma inf_apply (s : finset α) (f : α → Π (b : β), C b) (b : β) :
   s.inf f b = s.inf (λ a, f a b) :=
 @finset.sup_apply _ _ (λ b, order_dual (C b)) _ s f b
@@ -475,7 +477,8 @@ end inf
 section sup'
 variables {C : β → Type*} [Π (b : β), semilattice_sup (C b)]
 
-lemma sup'_apply {s : finset α} (H : s.nonempty) (f : α → Π (b : β), C b) (b : β) :
+@[simp]
+protected lemma sup'_apply {s : finset α} (H : s.nonempty) (f : α → Π (b : β), C b) (b : β) :
   s.sup' H f b = s.sup' H (λ a, f a b) :=
 comp_sup'_eq_sup'_comp H (λ x : Π b : β, C b, x b) (λ i j, rfl)
 
@@ -484,9 +487,10 @@ end sup'
 section inf'
 variables {C : β → Type*} [Π (b : β), semilattice_inf (C b)]
 
-lemma inf'_apply {s : finset α} (H : s.nonempty) (f : α → Π (b : β), C b) (b : β) :
+@[simp]
+protected lemma inf'_apply {s : finset α} (H : s.nonempty) (f : α → Π (b : β), C b) (b : β) :
   s.inf' H f b = s.inf' H (λ a, f a b) :=
-@sup'_apply _ _ (λ b, order_dual (C b)) _ _ H f b
+@finset.sup'_apply _ _ (λ b, order_dual (C b)) _ _ H f b
 
 end inf'
 
diff --git a/src/topology/continuous_function/basic.lean b/src/topology/continuous_function/basic.lean
index cf58db6b6c32d..e4488cf8c85fb 100644
--- a/src/topology/continuous_function/basic.lean
+++ b/src/topology/continuous_function/basic.lean
@@ -130,6 +130,10 @@ pi.lt_def
 instance has_sup [linear_order β] [order_closed_topology β] : has_sup C(α, β) :=
 { sup := λ f g, { to_fun := λ a, max (f a) (g a), } }
 
+@[simp, norm_cast] lemma sup_coe [linear_order β] [order_closed_topology β] (f g : C(α, β)) :
+  ((f ⊔ g : C(α, β)) : α → β) = (f ⊔ g : α → β) :=
+rfl
+
 @[simp] lemma sup_apply [linear_order β] [order_closed_topology β] (f g : C(α, β)) (a : α) :
   (f ⊔ g) a = max (f a) (g a) :=
 rfl
@@ -144,6 +148,10 @@ instance [linear_order β] [order_closed_topology β] : semilattice_sup C(α, β
 instance has_inf [linear_order β] [order_closed_topology β] : has_inf C(α, β) :=
 { inf := λ f g, { to_fun := λ a, min (f a) (g a), } }
 
+@[simp, norm_cast] lemma inf_coe [linear_order β] [order_closed_topology β] (f g : C(α, β)) :
+  ((f ⊓ g : C(α, β)) : α → β) = (f ⊓ g : α → β) :=
+rfl
+
 @[simp] lemma inf_apply [linear_order β] [order_closed_topology β] (f g : C(α, β)) (a : α) :
   (f ⊓ g) a = min (f a) (g a) :=
 rfl
@@ -161,6 +169,34 @@ instance [linear_order β] [order_closed_topology β] : lattice C(α, β) :=
 
 -- TODO transfer this lattice structure to `bounded_continuous_function`
 
+section sup'
+variables [linear_order γ] [order_closed_topology γ]
+
+lemma sup'_apply {ι : Type*} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) (b : β) :
+  s.sup' H f b = s.sup' H (λ a, f a b) :=
+finset.comp_sup'_eq_sup'_comp H (λ f : C(β, γ), f b) (λ i j, rfl)
+
+@[simp, norm_cast]
+lemma sup'_coe {ι : Type*} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) :
+  ((s.sup' H f : C(β, γ)) : ι → β) = s.sup' H (λ a, (f a : β → γ)) :=
+by { ext, simp [sup'_apply], }
+
+end sup'
+
+section inf'
+variables [linear_order γ] [order_closed_topology γ]
+
+lemma inf'_apply {ι : Type*} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) (b : β) :
+  s.inf' H f b = s.inf' H (λ a, f a b) :=
+@sup'_apply _ (order_dual γ) _ _ _ _ _ _ H f b
+
+@[simp, norm_cast]
+lemma inf'_coe {ι : Type*} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) :
+  ((s.inf' H f : C(β, γ)) : ι → β) = s.inf' H (λ a, (f a : β → γ)) :=
+@sup'_coe _ (order_dual γ) _ _ _ _ _ _ H f
+
+end inf'
+
 end lattice
 
 end continuous_map