Documentation

Mathlib.Topology.Order.Lattice

Topological lattices #

In this file we define mixin classes ContinuousInf and ContinuousSup. We define the class TopologicalLattice as a topological space and lattice L extending ContinuousInf and ContinuousSup.

References #

Tags #

topological, lattice

class ContinuousInf (L : Type u_1) [TopologicalSpace L] [Inf L] :

Let L be a topological space and let L×L be equipped with the product topology and let ⊓:L×L → L be an infimum. Then L is said to have (jointly) continuous infimum if the map ⊓:L×L → L is continuous.

  • continuous_inf : Continuous fun (p : L × L) => p.1 p.2

    The infimum is continuous

Instances
    theorem ContinuousInf.continuous_inf {L : Type u_1} :
    ∀ {inst : TopologicalSpace L} {inst_1 : Inf L} [self : ContinuousInf L], Continuous fun (p : L × L) => p.1 p.2

    The infimum is continuous

    class ContinuousSup (L : Type u_1) [TopologicalSpace L] [Sup L] :

    Let L be a topological space and let L×L be equipped with the product topology and let ⊓:L×L → L be a supremum. Then L is said to have (jointly) continuous supremum if the map ⊓:L×L → L is continuous.

    • continuous_sup : Continuous fun (p : L × L) => p.1 p.2

      The supremum is continuous

    Instances
      theorem ContinuousSup.continuous_sup {L : Type u_1} :
      ∀ {inst : TopologicalSpace L} {inst_1 : Sup L} [self : ContinuousSup L], Continuous fun (p : L × L) => p.1 p.2

      The supremum is continuous

      @[instance 100]
      Equations
      • =
      @[instance 100]
      Equations
      • =

      Let L be a lattice equipped with a topology such that L has continuous infimum and supremum. Then L is said to be a topological lattice.

        Instances
          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          theorem continuous_inf {L : Type u_1} [TopologicalSpace L] [Inf L] [ContinuousInf L] :
          Continuous fun (p : L × L) => p.1 p.2
          theorem Continuous.inf {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Inf L] [ContinuousInf L] {f : XL} {g : XL} (hf : Continuous f) (hg : Continuous g) :
          Continuous fun (x : X) => f x g x
          theorem continuous_sup {L : Type u_1} [TopologicalSpace L] [Sup L] [ContinuousSup L] :
          Continuous fun (p : L × L) => p.1 p.2
          theorem Continuous.sup {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Sup L] [ContinuousSup L] {f : XL} {g : XL} (hf : Continuous f) (hg : Continuous g) :
          Continuous fun (x : X) => f x g x
          theorem Filter.Tendsto.sup_nhds' {L : Type u_1} [TopologicalSpace L] {α : Type u_3} {l : Filter α} {f : αL} {g : αL} {x : L} {y : L} [Sup L] [ContinuousSup L] (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) :
          Filter.Tendsto (f g) l (nhds (x y))
          theorem Filter.Tendsto.sup_nhds {L : Type u_1} [TopologicalSpace L] {α : Type u_3} {l : Filter α} {f : αL} {g : αL} {x : L} {y : L} [Sup L] [ContinuousSup L] (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) :
          Filter.Tendsto (fun (i : α) => f i g i) l (nhds (x y))
          theorem Filter.Tendsto.inf_nhds' {L : Type u_1} [TopologicalSpace L] {α : Type u_3} {l : Filter α} {f : αL} {g : αL} {x : L} {y : L} [Inf L] [ContinuousInf L] (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) :
          Filter.Tendsto (f g) l (nhds (x y))
          theorem Filter.Tendsto.inf_nhds {L : Type u_1} [TopologicalSpace L] {α : Type u_3} {l : Filter α} {f : αL} {g : αL} {x : L} {y : L} [Inf L] [ContinuousInf L] (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) :
          Filter.Tendsto (fun (i : α) => f i g i) l (nhds (x y))
          theorem Filter.Tendsto.finset_sup'_nhds {L : Type u_1} [TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ιαL} {l : Filter α} {g : ιL} [SemilatticeSup L] [ContinuousSup L] (hne : s.Nonempty) (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
          Filter.Tendsto (s.sup' hne f) l (nhds (s.sup' hne g))
          theorem Filter.Tendsto.finset_sup'_nhds_apply {L : Type u_1} [TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ιαL} {l : Filter α} {g : ιL} [SemilatticeSup L] [ContinuousSup L] (hne : s.Nonempty) (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
          Filter.Tendsto (fun (a : α) => s.sup' hne fun (x : ι) => f x a) l (nhds (s.sup' hne g))
          theorem Filter.Tendsto.finset_inf'_nhds {L : Type u_1} [TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ιαL} {l : Filter α} {g : ιL} [SemilatticeInf L] [ContinuousInf L] (hne : s.Nonempty) (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
          Filter.Tendsto (s.inf' hne f) l (nhds (s.inf' hne g))
          theorem Filter.Tendsto.finset_inf'_nhds_apply {L : Type u_1} [TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ιαL} {l : Filter α} {g : ιL} [SemilatticeInf L] [ContinuousInf L] (hne : s.Nonempty) (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
          Filter.Tendsto (fun (a : α) => s.inf' hne fun (x : ι) => f x a) l (nhds (s.inf' hne g))
          theorem Filter.Tendsto.finset_sup_nhds {L : Type u_1} [TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ιαL} {l : Filter α} {g : ιL} [SemilatticeSup L] [OrderBot L] [ContinuousSup L] (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
          Filter.Tendsto (s.sup f) l (nhds (s.sup g))
          theorem Filter.Tendsto.finset_sup_nhds_apply {L : Type u_1} [TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ιαL} {l : Filter α} {g : ιL} [SemilatticeSup L] [OrderBot L] [ContinuousSup L] (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
          Filter.Tendsto (fun (a : α) => s.sup fun (x : ι) => f x a) l (nhds (s.sup g))
          theorem Filter.Tendsto.finset_inf_nhds {L : Type u_1} [TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ιαL} {l : Filter α} {g : ιL} [SemilatticeInf L] [OrderTop L] [ContinuousInf L] (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
          Filter.Tendsto (s.inf f) l (nhds (s.inf g))
          theorem Filter.Tendsto.finset_inf_nhds_apply {L : Type u_1} [TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ιαL} {l : Filter α} {g : ιL} [SemilatticeInf L] [OrderTop L] [ContinuousInf L] (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
          Filter.Tendsto (fun (a : α) => s.inf fun (x : ι) => f x a) l (nhds (s.inf g))
          theorem ContinuousAt.sup' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Sup L] [ContinuousSup L] {f : XL} {g : XL} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
          theorem ContinuousAt.sup {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Sup L] [ContinuousSup L] {f : XL} {g : XL} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
          ContinuousAt (fun (a : X) => f a g a) x
          theorem ContinuousWithinAt.sup' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Sup L] [ContinuousSup L] {f : XL} {g : XL} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
          theorem ContinuousWithinAt.sup {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Sup L] [ContinuousSup L] {f : XL} {g : XL} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
          ContinuousWithinAt (fun (a : X) => f a g a) s x
          theorem ContinuousOn.sup' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Sup L] [ContinuousSup L] {f : XL} {g : XL} {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
          theorem ContinuousOn.sup {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Sup L] [ContinuousSup L] {f : XL} {g : XL} {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
          ContinuousOn (fun (a : X) => f a g a) s
          theorem Continuous.sup' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Sup L] [ContinuousSup L] {f : XL} {g : XL} (hf : Continuous f) (hg : Continuous g) :
          theorem ContinuousAt.inf' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Inf L] [ContinuousInf L] {f : XL} {g : XL} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
          theorem ContinuousAt.inf {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Inf L] [ContinuousInf L] {f : XL} {g : XL} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
          ContinuousAt (fun (a : X) => f a g a) x
          theorem ContinuousWithinAt.inf' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Inf L] [ContinuousInf L] {f : XL} {g : XL} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
          theorem ContinuousWithinAt.inf {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Inf L] [ContinuousInf L] {f : XL} {g : XL} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
          ContinuousWithinAt (fun (a : X) => f a g a) s x
          theorem ContinuousOn.inf' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Inf L] [ContinuousInf L] {f : XL} {g : XL} {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
          theorem ContinuousOn.inf {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Inf L] [ContinuousInf L] {f : XL} {g : XL} {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
          ContinuousOn (fun (a : X) => f a g a) s
          theorem Continuous.inf' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Inf L] [ContinuousInf L] {f : XL} {g : XL} (hf : Continuous f) (hg : Continuous g) :
          theorem ContinuousAt.finset_sup'_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ιXL} {x : X} (hne : s.Nonempty) (hs : is, ContinuousAt (f i) x) :
          ContinuousAt (fun (a : X) => s.sup' hne fun (x : ι) => f x a) x
          theorem ContinuousAt.finset_sup' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ιXL} {x : X} (hne : s.Nonempty) (hs : is, ContinuousAt (f i) x) :
          ContinuousAt (s.sup' hne f) x
          theorem ContinuousWithinAt.finset_sup'_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ιXL} {t : Set X} {x : X} (hne : s.Nonempty) (hs : is, ContinuousWithinAt (f i) t x) :
          ContinuousWithinAt (fun (a : X) => s.sup' hne fun (x : ι) => f x a) t x
          theorem ContinuousWithinAt.finset_sup' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ιXL} {t : Set X} {x : X} (hne : s.Nonempty) (hs : is, ContinuousWithinAt (f i) t x) :
          ContinuousWithinAt (s.sup' hne f) t x
          theorem ContinuousOn.finset_sup'_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ιXL} {t : Set X} (hne : s.Nonempty) (hs : is, ContinuousOn (f i) t) :
          ContinuousOn (fun (a : X) => s.sup' hne fun (x : ι) => f x a) t
          theorem ContinuousOn.finset_sup' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ιXL} {t : Set X} (hne : s.Nonempty) (hs : is, ContinuousOn (f i) t) :
          ContinuousOn (s.sup' hne f) t
          theorem Continuous.finset_sup'_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ιXL} (hne : s.Nonempty) (hs : is, Continuous (f i)) :
          Continuous fun (a : X) => s.sup' hne fun (x : ι) => f x a
          theorem Continuous.finset_sup' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ιXL} (hne : s.Nonempty) (hs : is, Continuous (f i)) :
          Continuous (s.sup' hne f)
          theorem ContinuousAt.finset_sup_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ιXL} {x : X} (hs : is, ContinuousAt (f i) x) :
          ContinuousAt (fun (a : X) => s.sup fun (x : ι) => f x a) x
          theorem ContinuousAt.finset_sup {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ιXL} {x : X} (hs : is, ContinuousAt (f i) x) :
          ContinuousAt (s.sup f) x
          theorem ContinuousWithinAt.finset_sup_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ιXL} {t : Set X} {x : X} (hs : is, ContinuousWithinAt (f i) t x) :
          ContinuousWithinAt (fun (a : X) => s.sup fun (x : ι) => f x a) t x
          theorem ContinuousWithinAt.finset_sup {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ιXL} {t : Set X} {x : X} (hs : is, ContinuousWithinAt (f i) t x) :
          ContinuousWithinAt (s.sup f) t x
          theorem ContinuousOn.finset_sup_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ιXL} {t : Set X} (hs : is, ContinuousOn (f i) t) :
          ContinuousOn (fun (a : X) => s.sup fun (x : ι) => f x a) t
          theorem ContinuousOn.finset_sup {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ιXL} {t : Set X} (hs : is, ContinuousOn (f i) t) :
          ContinuousOn (s.sup f) t
          theorem Continuous.finset_sup_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ιXL} (hs : is, Continuous (f i)) :
          Continuous fun (a : X) => s.sup fun (x : ι) => f x a
          theorem Continuous.finset_sup {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup L] [OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ιXL} (hs : is, Continuous (f i)) :
          Continuous (s.sup f)
          theorem ContinuousAt.finset_inf'_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ιXL} {x : X} (hne : s.Nonempty) (hs : is, ContinuousAt (f i) x) :
          ContinuousAt (fun (a : X) => s.inf' hne fun (x : ι) => f x a) x
          theorem ContinuousAt.finset_inf' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ιXL} {x : X} (hne : s.Nonempty) (hs : is, ContinuousAt (f i) x) :
          ContinuousAt (s.inf' hne f) x
          theorem ContinuousWithinAt.finset_inf'_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ιXL} {t : Set X} {x : X} (hne : s.Nonempty) (hs : is, ContinuousWithinAt (f i) t x) :
          ContinuousWithinAt (fun (a : X) => s.inf' hne fun (x : ι) => f x a) t x
          theorem ContinuousWithinAt.finset_inf' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ιXL} {t : Set X} {x : X} (hne : s.Nonempty) (hs : is, ContinuousWithinAt (f i) t x) :
          ContinuousWithinAt (s.inf' hne f) t x
          theorem ContinuousOn.finset_inf'_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ιXL} {t : Set X} (hne : s.Nonempty) (hs : is, ContinuousOn (f i) t) :
          ContinuousOn (fun (a : X) => s.inf' hne fun (x : ι) => f x a) t
          theorem ContinuousOn.finset_inf' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ιXL} {t : Set X} (hne : s.Nonempty) (hs : is, ContinuousOn (f i) t) :
          ContinuousOn (s.inf' hne f) t
          theorem Continuous.finset_inf'_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ιXL} (hne : s.Nonempty) (hs : is, Continuous (f i)) :
          Continuous fun (a : X) => s.inf' hne fun (x : ι) => f x a
          theorem Continuous.finset_inf' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ιXL} (hne : s.Nonempty) (hs : is, Continuous (f i)) :
          Continuous (s.inf' hne f)
          theorem ContinuousAt.finset_inf_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ιXL} {x : X} (hs : is, ContinuousAt (f i) x) :
          ContinuousAt (fun (a : X) => s.inf fun (x : ι) => f x a) x
          theorem ContinuousAt.finset_inf {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ιXL} {x : X} (hs : is, ContinuousAt (f i) x) :
          ContinuousAt (s.inf f) x
          theorem ContinuousWithinAt.finset_inf_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ιXL} {t : Set X} {x : X} (hs : is, ContinuousWithinAt (f i) t x) :
          ContinuousWithinAt (fun (a : X) => s.inf fun (x : ι) => f x a) t x
          theorem ContinuousWithinAt.finset_inf {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ιXL} {t : Set X} {x : X} (hs : is, ContinuousWithinAt (f i) t x) :
          ContinuousWithinAt (s.inf f) t x
          theorem ContinuousOn.finset_inf_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ιXL} {t : Set X} (hs : is, ContinuousOn (f i) t) :
          ContinuousOn (fun (a : X) => s.inf fun (x : ι) => f x a) t
          theorem ContinuousOn.finset_inf {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ιXL} {t : Set X} (hs : is, ContinuousOn (f i) t) :
          ContinuousOn (s.inf f) t
          theorem Continuous.finset_inf_apply {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ιXL} (hs : is, Continuous (f i)) :
          Continuous fun (a : X) => s.inf fun (x : ι) => f x a
          theorem Continuous.finset_inf {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf L] [OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ιXL} (hs : is, Continuous (f i)) :
          Continuous (s.inf f)