chore(Topology/Order/Lattice): tag continuity lemmas with fun_prop (leanprover-community#33682)

Author: gasparattila

Mathlib/Topology/Order/Lattice.lean

@@ -172,6 +172,7 @@ section Sup
 
 variable [Max L] [ContinuousSup L] {f g : X → L} {s : Set X} {x : X}
 
+@[fun_prop]
 lemma ContinuousAt.sup' (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
     ContinuousAt (f ⊔ g) x :=
   hf.sup_nhds' hg
@@ -181,14 +182,17 @@ lemma ContinuousAt.sup (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
     ContinuousAt (fun a ↦ f a ⊔ g a) x :=
   hf.sup' hg
 
+@[fun_prop]
 lemma ContinuousWithinAt.sup' (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
     ContinuousWithinAt (f ⊔ g) s x :=
   hf.sup_nhds' hg
 
+@[fun_prop]
 lemma ContinuousWithinAt.sup (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
     ContinuousWithinAt (fun a ↦ f a ⊔ g a) s x :=
   hf.sup' hg
 
+@[fun_prop]
 lemma ContinuousOn.sup' (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
     ContinuousOn (f ⊔ g) s := fun x hx ↦
   (hf x hx).sup' (hg x hx)
@@ -198,6 +202,7 @@ lemma ContinuousOn.sup (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
     ContinuousOn (fun a ↦ f a ⊔ g a) s :=
   hf.sup' hg
 
+@[fun_prop]
 lemma Continuous.sup' (hf : Continuous f) (hg : Continuous g) : Continuous (f ⊔ g) := hf.sup hg
 
 end Sup
@@ -206,6 +211,7 @@ section Inf
 
 variable [Min L] [ContinuousInf L] {f g : X → L} {s : Set X} {x : X}
 
+@[fun_prop]
 lemma ContinuousAt.inf' (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
     ContinuousAt (f ⊓ g) x :=
   hf.inf_nhds' hg
@@ -215,14 +221,17 @@ lemma ContinuousAt.inf (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
     ContinuousAt (fun a ↦ f a ⊓ g a) x :=
   hf.inf' hg
 
+@[fun_prop]
 lemma ContinuousWithinAt.inf' (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
     ContinuousWithinAt (f ⊓ g) s x :=
   hf.inf_nhds' hg
 
+@[fun_prop]
 lemma ContinuousWithinAt.inf (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
     ContinuousWithinAt (fun a ↦ f a ⊓ g a) s x :=
   hf.inf' hg
 
+@[fun_prop]
 lemma ContinuousOn.inf' (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
     ContinuousOn (f ⊓ g) s := fun x hx ↦
   (hf x hx).inf' (hg x hx)
@@ -232,6 +241,7 @@ lemma ContinuousOn.inf (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
     ContinuousOn (fun a ↦ f a ⊓ g a) s :=
   hf.inf' hg
 
+@[fun_prop]
 lemma Continuous.inf' (hf : Continuous f) (hg : Continuous g) : Continuous (f ⊓ g) := hf.inf hg
 
 end Inf
@@ -241,36 +251,44 @@ section FinsetSup'
 variable {ι : Type*} [SemilatticeSup L] [ContinuousSup L] {s : Finset ι}
   {f : ι → X → L} {t : Set X} {x : X}
 
+@[fun_prop]
 lemma ContinuousAt.finset_sup'_apply (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
     ContinuousAt (fun a ↦ s.sup' hne (f · a)) x :=
   Tendsto.finset_sup'_nhds_apply hne hs
 
+@[fun_prop]
 lemma ContinuousAt.finset_sup' (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
     ContinuousAt (s.sup' hne f) x := by
   simpa only [← Finset.sup'_apply] using finset_sup'_apply hne hs
 
+@[fun_prop]
 lemma ContinuousWithinAt.finset_sup'_apply (hne : s.Nonempty)
     (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) :
     ContinuousWithinAt (fun a ↦ s.sup' hne (f · a)) t x :=
   Tendsto.finset_sup'_nhds_apply hne hs
 
+@[fun_prop]
 lemma ContinuousWithinAt.finset_sup' (hne : s.Nonempty)
     (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) : ContinuousWithinAt (s.sup' hne f) t x := by
   simpa only [← Finset.sup'_apply] using finset_sup'_apply hne hs
 
+@[fun_prop]
 lemma ContinuousOn.finset_sup'_apply (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousOn (f i) t) :
     ContinuousOn (fun a ↦ s.sup' hne (f · a)) t := fun x hx ↦
   ContinuousWithinAt.finset_sup'_apply hne fun i hi ↦ hs i hi x hx
 
+@[fun_prop]
 lemma ContinuousOn.finset_sup' (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousOn (f i) t) :
     ContinuousOn (s.sup' hne f) t := fun x hx ↦
   ContinuousWithinAt.finset_sup' hne fun i hi ↦ hs i hi x hx
 
+@[fun_prop]
 lemma Continuous.finset_sup'_apply (hne : s.Nonempty) (hs : ∀ i ∈ s, Continuous (f i)) :
     Continuous (fun a ↦ s.sup' hne (f · a)) :=
   continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_sup'_apply _ fun i hi ↦
     (hs i hi).continuousAt
 
+@[fun_prop]
 lemma Continuous.finset_sup' (hne : s.Nonempty) (hs : ∀ i ∈ s, Continuous (f i)) :
     Continuous (s.sup' hne f) :=
   continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_sup' _ fun i hi ↦ (hs i hi).continuousAt
@@ -282,36 +300,44 @@ section FinsetSup
 variable {ι : Type*} [SemilatticeSup L] [OrderBot L] [ContinuousSup L] {s : Finset ι}
   {f : ι → X → L} {t : Set X} {x : X}
 
+@[fun_prop]
 lemma ContinuousAt.finset_sup_apply (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
     ContinuousAt (fun a ↦ s.sup (f · a)) x :=
   Tendsto.finset_sup_nhds_apply hs
 
+@[fun_prop]
 lemma ContinuousAt.finset_sup (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
     ContinuousAt (s.sup f) x := by
   simpa only [← Finset.sup_apply] using finset_sup_apply hs
 
+@[fun_prop]
 lemma ContinuousWithinAt.finset_sup_apply
     (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) :
     ContinuousWithinAt (fun a ↦ s.sup (f · a)) t x :=
   Tendsto.finset_sup_nhds_apply hs
 
+@[fun_prop]
 lemma ContinuousWithinAt.finset_sup
     (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) : ContinuousWithinAt (s.sup f) t x := by
   simpa only [← Finset.sup_apply] using finset_sup_apply hs
 
+@[fun_prop]
 lemma ContinuousOn.finset_sup_apply (hs : ∀ i ∈ s, ContinuousOn (f i) t) :
     ContinuousOn (fun a ↦ s.sup (f · a)) t := fun x hx ↦
   ContinuousWithinAt.finset_sup_apply fun i hi ↦ hs i hi x hx
 
+@[fun_prop]
 lemma ContinuousOn.finset_sup (hs : ∀ i ∈ s, ContinuousOn (f i) t) :
     ContinuousOn (s.sup f) t := fun x hx ↦
   ContinuousWithinAt.finset_sup fun i hi ↦ hs i hi x hx
 
+@[fun_prop]
 lemma Continuous.finset_sup_apply (hs : ∀ i ∈ s, Continuous (f i)) :
     Continuous (fun a ↦ s.sup (f · a)) :=
   continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_sup_apply fun i hi ↦
     (hs i hi).continuousAt
 
+@[fun_prop]
 lemma Continuous.finset_sup (hs : ∀ i ∈ s, Continuous (f i)) : Continuous (s.sup f) :=
   continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_sup fun i hi ↦ (hs i hi).continuousAt
 
@@ -322,36 +348,44 @@ section FinsetInf'
 variable {ι : Type*} [SemilatticeInf L] [ContinuousInf L] {s : Finset ι}
   {f : ι → X → L} {t : Set X} {x : X}
 
+@[fun_prop]
 lemma ContinuousAt.finset_inf'_apply (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
     ContinuousAt (fun a ↦ s.inf' hne (f · a)) x :=
   Tendsto.finset_inf'_nhds_apply hne hs
 
+@[fun_prop]
 lemma ContinuousAt.finset_inf' (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
     ContinuousAt (s.inf' hne f) x := by
   simpa only [← Finset.inf'_apply] using finset_inf'_apply hne hs
 
+@[fun_prop]
 lemma ContinuousWithinAt.finset_inf'_apply (hne : s.Nonempty)
     (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) :
     ContinuousWithinAt (fun a ↦ s.inf' hne (f · a)) t x :=
   Tendsto.finset_inf'_nhds_apply hne hs
 
+@[fun_prop]
 lemma ContinuousWithinAt.finset_inf' (hne : s.Nonempty)
     (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) : ContinuousWithinAt (s.inf' hne f) t x := by
   simpa only [← Finset.inf'_apply] using finset_inf'_apply hne hs
 
+@[fun_prop]
 lemma ContinuousOn.finset_inf'_apply (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousOn (f i) t) :
     ContinuousOn (fun a ↦ s.inf' hne (f · a)) t := fun x hx ↦
   ContinuousWithinAt.finset_inf'_apply hne fun i hi ↦ hs i hi x hx
 
+@[fun_prop]
 lemma ContinuousOn.finset_inf' (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousOn (f i) t) :
     ContinuousOn (s.inf' hne f) t := fun x hx ↦
   ContinuousWithinAt.finset_inf' hne fun i hi ↦ hs i hi x hx
 
+@[fun_prop]
 lemma Continuous.finset_inf'_apply (hne : s.Nonempty) (hs : ∀ i ∈ s, Continuous (f i)) :
     Continuous (fun a ↦ s.inf' hne (f · a)) :=
   continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_inf'_apply _ fun i hi ↦
     (hs i hi).continuousAt
 
+@[fun_prop]
 lemma Continuous.finset_inf' (hne : s.Nonempty) (hs : ∀ i ∈ s, Continuous (f i)) :
     Continuous (s.inf' hne f) :=
   continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_inf' _ fun i hi ↦ (hs i hi).continuousAt
@@ -363,36 +397,44 @@ section FinsetInf
 variable {ι : Type*} [SemilatticeInf L] [OrderTop L] [ContinuousInf L] {s : Finset ι}
   {f : ι → X → L} {t : Set X} {x : X}
 
+@[fun_prop]
 lemma ContinuousAt.finset_inf_apply (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
     ContinuousAt (fun a ↦ s.inf (f · a)) x :=
   Tendsto.finset_inf_nhds_apply hs
 
+@[fun_prop]
 lemma ContinuousAt.finset_inf (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
     ContinuousAt (s.inf f) x := by
   simpa only [← Finset.inf_apply] using finset_inf_apply hs
 
+@[fun_prop]
 lemma ContinuousWithinAt.finset_inf_apply
     (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) :
     ContinuousWithinAt (fun a ↦ s.inf (f · a)) t x :=
   Tendsto.finset_inf_nhds_apply hs
 
+@[fun_prop]
 lemma ContinuousWithinAt.finset_inf
     (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) : ContinuousWithinAt (s.inf f) t x := by
   simpa only [← Finset.inf_apply] using finset_inf_apply hs
 
+@[fun_prop]
 lemma ContinuousOn.finset_inf_apply (hs : ∀ i ∈ s, ContinuousOn (f i) t) :
     ContinuousOn (fun a ↦ s.inf (f · a)) t := fun x hx ↦
   ContinuousWithinAt.finset_inf_apply fun i hi ↦ hs i hi x hx
 
+@[fun_prop]
 lemma ContinuousOn.finset_inf (hs : ∀ i ∈ s, ContinuousOn (f i) t) :
     ContinuousOn (s.inf f) t := fun x hx ↦
   ContinuousWithinAt.finset_inf fun i hi ↦ hs i hi x hx
 
+@[fun_prop]
 lemma Continuous.finset_inf_apply (hs : ∀ i ∈ s, Continuous (f i)) :
     Continuous (fun a ↦ s.inf (f · a)) :=
   continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_inf_apply fun i hi ↦
     (hs i hi).continuousAt
 
+@[fun_prop]
 lemma Continuous.finset_inf (hs : ∀ i ∈ s, Continuous (f i)) : Continuous (s.inf f) :=
   continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_inf fun i hi ↦ (hs i hi).continuousAt