feat(Topology/Order): continuity of Finset.sup, partialSups etc (#…

…8141)

Also rename `Filter.Tendsto.sup_right_nhds` to `Filter.Tendsto.sup_nhds` etc.

Mathlib.lean

@@ -3605,6 +3605,7 @@ import Mathlib.Topology.Order.Hom.Esakia
 import Mathlib.Topology.Order.Lattice
 import Mathlib.Topology.Order.LowerUpperTopology
 import Mathlib.Topology.Order.NhdsSet
+import Mathlib.Topology.Order.PartialSups
 import Mathlib.Topology.Order.Priestley
 import Mathlib.Topology.Order.UpperLowerSetTopology
 import Mathlib.Topology.Partial

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -546,14 +546,14 @@ open Filter
 protected theorem sup [Sup β] [ContinuousSup β] (hf : StronglyMeasurable f)
     (hg : StronglyMeasurable g) : StronglyMeasurable (f ⊔ g) :=
   ⟨fun n => hf.approx n ⊔ hg.approx n, fun x =>
-    (hf.tendsto_approx x).sup_right_nhds (hg.tendsto_approx x)⟩
+    (hf.tendsto_approx x).sup_nhds (hg.tendsto_approx x)⟩
 #align measure_theory.strongly_measurable.sup MeasureTheory.StronglyMeasurable.sup
 
 @[aesop safe 20 (rule_sets [Measurable])]
 protected theorem inf [Inf β] [ContinuousInf β] (hf : StronglyMeasurable f)
     (hg : StronglyMeasurable g) : StronglyMeasurable (f ⊓ g) :=
   ⟨fun n => hf.approx n ⊓ hg.approx n, fun x =>
-    (hf.tendsto_approx x).inf_right_nhds (hg.tendsto_approx x)⟩
+    (hf.tendsto_approx x).inf_nhds (hg.tendsto_approx x)⟩
 #align measure_theory.strongly_measurable.inf MeasureTheory.StronglyMeasurable.inf
 
 end Order
@@ -1120,7 +1120,7 @@ protected theorem sup [SemilatticeSup β] [ContinuousSup β] (hf : FinStronglyMe
     (hg : FinStronglyMeasurable g μ) : FinStronglyMeasurable (f ⊔ g) μ := by
   refine'
     ⟨fun n => hf.approx n ⊔ hg.approx n, fun n => _, fun x =>
-      (hf.tendsto_approx x).sup_right_nhds (hg.tendsto_approx x)⟩
+      (hf.tendsto_approx x).sup_nhds (hg.tendsto_approx x)⟩
   refine' (measure_mono (support_sup _ _)).trans_lt _
   exact measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩
 #align measure_theory.fin_strongly_measurable.sup MeasureTheory.FinStronglyMeasurable.sup
@@ -1130,7 +1130,7 @@ protected theorem inf [SemilatticeInf β] [ContinuousInf β] (hf : FinStronglyMe
     (hg : FinStronglyMeasurable g μ) : FinStronglyMeasurable (f ⊓ g) μ := by
   refine'
     ⟨fun n => hf.approx n ⊓ hg.approx n, fun n => _, fun x =>
-      (hf.tendsto_approx x).inf_right_nhds (hg.tendsto_approx x)⟩
+      (hf.tendsto_approx x).inf_nhds (hg.tendsto_approx x)⟩
   refine' (measure_mono (support_inf _ _)).trans_lt _
   exact measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩
 #align measure_theory.fin_strongly_measurable.inf MeasureTheory.FinStronglyMeasurable.inf

Mathlib/Order/PartialSups.lean

@@ -122,6 +122,10 @@ theorem partialSups_eq_sup'_range (f : ℕ → α) (n : ℕ) :
   eq_of_forall_ge_iff fun _ ↦ by simp [Nat.lt_succ_iff]
 #align partial_sups_eq_sup'_range partialSups_eq_sup'_range
 
+lemma partialSups_apply {ι : Type*} {π : ι → Type*} [(i : ι) → SemilatticeSup (π i)]
+    (f : ℕ → (i : ι) → π i) (n : ℕ) (i : ι) : partialSups f n i = partialSups (f · i) n := by
+  simp only [partialSups_eq_sup'_range, Finset.sup'_apply]
+
 end SemilatticeSup
 
 theorem partialSups_eq_sup_range [SemilatticeSup α] [OrderBot α] (f : ℕ → α) (n : ℕ) :

Mathlib/Topology/Order/Lattice.lean

@@ -26,7 +26,6 @@ topological, lattice
 
 set_option autoImplicit true
 
-
 open Filter
 
 open Topology
@@ -75,8 +74,7 @@ instance (priority := 100) OrderDual.topologicalLattice (L : Type*) [Topological
 
 -- see Note [lower instance priority]
 instance (priority := 100) LinearOrder.topologicalLattice {L : Type*} [TopologicalSpace L]
-    [LinearOrder L] [OrderClosedTopology L] : TopologicalLattice L
-    where
+    [LinearOrder L] [OrderClosedTopology L] : TopologicalLattice L where
   continuous_inf := continuous_min
   continuous_sup := continuous_max
 #align linear_order.topological_lattice LinearOrder.topologicalLattice
@@ -105,26 +103,308 @@ theorem Continuous.sup [Sup L] [ContinuousSup L] {f g : X → L} (hf : Continuou
   continuous_sup.comp (hf.prod_mk hg : _)
 #align continuous.sup Continuous.sup
 
-theorem Filter.Tendsto.sup_right_nhds' {ι β} [TopologicalSpace β] [Sup β] [ContinuousSup β]
-    {l : Filter ι} {f g : ι → β} {x y : β} (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
+namespace Filter.Tendsto
+
+section SupInf
+
+variable {α : Type*} {l : Filter α} {f g : α → L} {x y : L}
+
+lemma sup_nhds' [Sup L] [ContinuousSup L] (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
     Tendsto (f ⊔ g) l (𝓝 (x ⊔ y)) :=
   (continuous_sup.tendsto _).comp (Tendsto.prod_mk_nhds hf hg)
-#align filter.tendsto.sup_right_nhds' Filter.Tendsto.sup_right_nhds'
+#align filter.tendsto.sup_right_nhds' Filter.Tendsto.sup_nhds'
 
-theorem Filter.Tendsto.sup_right_nhds {ι β} [TopologicalSpace β] [Sup β] [ContinuousSup β]
-    {l : Filter ι} {f g : ι → β} {x y : β} (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
+lemma sup_nhds [Sup L] [ContinuousSup L] (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
     Tendsto (fun i => f i ⊔ g i) l (𝓝 (x ⊔ y)) :=
-  hf.sup_right_nhds' hg
-#align filter.tendsto.sup_right_nhds Filter.Tendsto.sup_right_nhds
+  hf.sup_nhds' hg
+#align filter.tendsto.sup_right_nhds Filter.Tendsto.sup_nhds
 
-theorem Filter.Tendsto.inf_right_nhds' {ι β} [TopologicalSpace β] [Inf β] [ContinuousInf β]
-    {l : Filter ι} {f g : ι → β} {x y : β} (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
+lemma inf_nhds' [Inf L] [ContinuousInf L] (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
     Tendsto (f ⊓ g) l (𝓝 (x ⊓ y)) :=
   (continuous_inf.tendsto _).comp (Tendsto.prod_mk_nhds hf hg)
-#align filter.tendsto.inf_right_nhds' Filter.Tendsto.inf_right_nhds'
+#align filter.tendsto.inf_right_nhds' Filter.Tendsto.inf_nhds'
 
-theorem Filter.Tendsto.inf_right_nhds {ι β} [TopologicalSpace β] [Inf β] [ContinuousInf β]
-    {l : Filter ι} {f g : ι → β} {x y : β} (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
+lemma inf_nhds [Inf L] [ContinuousInf L] (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
     Tendsto (fun i => f i ⊓ g i) l (𝓝 (x ⊓ y)) :=
-  hf.inf_right_nhds' hg
-#align filter.tendsto.inf_right_nhds Filter.Tendsto.inf_right_nhds
+  hf.inf_nhds' hg
+#align filter.tendsto.inf_right_nhds Filter.Tendsto.inf_nhds
+
+end SupInf
+
+open Finset
+
+variable {ι : Type*} {s : Finset ι} {f : ι → α → L} {g : ι → L}
+
+lemma finset_sup'_nhds [SemilatticeSup L] [ContinuousSup L]
+    (hne : s.Nonempty) (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) :
+    Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g)) := by
+  induction hne using Finset.Nonempty.cons_induction with
+  | h₀ => simpa using hs
+  | h₁ s ha hne ihs =>
+    rw [forall_mem_cons] at hs
+    simp only [sup'_cons, hne]
+    exact hs.1.sup_nhds (ihs hs.2)
+
+lemma finset_sup'_nhds_apply [SemilatticeSup L] [ContinuousSup L]
+    (hne : s.Nonempty) (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) :
+    Tendsto (fun a ↦ s.sup' hne (f · a)) l (𝓝 (s.sup' hne g)) := by
+  simpa only [← Finset.sup'_apply] using finset_sup'_nhds hne hs
+
+lemma finset_inf'_nhds [SemilatticeInf L] [ContinuousInf L]
+    (hne : s.Nonempty) (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) :
+    Tendsto (s.inf' hne f) l (𝓝 (s.inf' hne g)) :=
+  finset_sup'_nhds (L := Lᵒᵈ) hne hs
+
+lemma finset_inf'_nhds_apply [SemilatticeInf L] [ContinuousInf L]
+    (hne : s.Nonempty) (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) :
+    Tendsto (fun a ↦ s.inf' hne (f · a)) l (𝓝 (s.inf' hne g)) :=
+  finset_sup'_nhds_apply (L := Lᵒᵈ) hne hs
+
+lemma finset_sup_nhds [SemilatticeSup L] [OrderBot L] [ContinuousSup L]
+    (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) : Tendsto (s.sup f) l (𝓝 (s.sup g)) := by
+  rcases s.eq_empty_or_nonempty with rfl | hne
+  · simpa using tendsto_const_nhds
+  · simp only [← sup'_eq_sup hne]
+    exact finset_sup'_nhds hne hs
+
+lemma finset_sup_nhds_apply [SemilatticeSup L] [OrderBot L] [ContinuousSup L]
+    (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) :
+    Tendsto (fun a ↦ s.sup (f · a)) l (𝓝 (s.sup g)) := by
+  simpa only [← Finset.sup_apply] using finset_sup_nhds hs
+
+lemma finset_inf_nhds [SemilatticeInf L] [OrderTop L] [ContinuousInf L]
+    (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) : Tendsto (s.inf f) l (𝓝 (s.inf g)) :=
+  finset_sup_nhds (L := Lᵒᵈ) hs
+
+lemma finset_inf_nhds_apply [SemilatticeInf L] [OrderTop L] [ContinuousInf L]
+    (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) :
+    Tendsto (fun a ↦ s.inf (f · a)) l (𝓝 (s.inf g)) :=
+  finset_sup_nhds_apply (L := Lᵒᵈ) hs
+
+end Filter.Tendsto
+
+section Sup
+
+variable [Sup L] [ContinuousSup L] {f g : X → L} {s : Set X} {x : X}
+
+lemma ContinuousAt.sup' (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
+    ContinuousAt (f ⊔ g) x :=
+  hf.sup_nhds' hg
+
+lemma ContinuousAt.sup (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
+    ContinuousAt (fun a ↦ f a ⊔ g a) x :=
+  hf.sup' hg
+
+lemma ContinuousWithinAt.sup' (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
+    ContinuousWithinAt (f ⊔ g) s x :=
+  hf.sup_nhds' hg
+
+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
+
+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)
+
+lemma ContinuousOn.sup (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
+    ContinuousOn (fun a ↦ f a ⊔ g a) s :=
+  hf.sup' hg
+
+lemma Continuous.sup' (hf : Continuous f) (hg : Continuous g) : Continuous (f ⊔ g) := hf.sup hg
+
+end Sup
+
+section Inf
+
+variable [Inf L] [ContinuousInf L] {f g : X → L} {s : Set X} {x : X}
+
+lemma ContinuousAt.inf' (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
+    ContinuousAt (f ⊓ g) x :=
+  hf.inf_nhds' hg
+
+lemma ContinuousAt.inf (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
+    ContinuousAt (fun a ↦ f a ⊓ g a) x :=
+  hf.inf' hg
+
+lemma ContinuousWithinAt.inf' (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
+    ContinuousWithinAt (f ⊓ g) s x :=
+  hf.inf_nhds' hg
+
+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
+
+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)
+
+lemma ContinuousOn.inf (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
+    ContinuousOn (fun a ↦ f a ⊓ g a) s :=
+  hf.inf' hg
+
+lemma Continuous.inf' (hf : Continuous f) (hg : Continuous g) : Continuous (f ⊓ g) := hf.inf hg
+
+end Inf
+
+section FinsetSup'
+
+variable {ι : Type*} [SemilatticeSup L] [ContinuousSup L] {s : Finset ι}
+  {f : ι → X → L} {t : Set X} {x : X}
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+end FinsetSup'
+
+section FinsetSup
+
+variable {ι : Type*} [SemilatticeSup L] [OrderBot L] [ContinuousSup L] {s : Finset ι}
+  {f : ι → X → L} {t : Set X} {x : X}
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+end FinsetSup
+
+section FinsetInf'
+
+variable {ι : Type*} [SemilatticeInf L] [ContinuousInf L] {s : Finset ι}
+  {f : ι → X → L} {t : Set X} {x : X}
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+end FinsetInf'
+
+section FinsetInf
+
+variable {ι : Type*} [SemilatticeInf L] [OrderTop L] [ContinuousInf L] {s : Finset ι}
+  {f : ι → X → L} {t : Set X} {x : X}
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+end FinsetInf