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

• Gierz et al, A Compendium of Continuous Lattices

Tags

topological, lattice

class ContinuousInf (L : Type u_1) [TopologicalSpace L] [Min L] : Prop

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

class ContinuousSup (L : Type u_1) [TopologicalSpace L] [Max L] : Prop

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

instance OrderDual.continuousSup (L : Type u_1) [TopologicalSpace L] [Min L] [h : ContinuousInf L] : ContinuousSup Lᵒᵈ

instance OrderDual.continuousInf (L : Type u_1) [TopologicalSpace L] [Max L] [h : ContinuousSup L] : ContinuousInf Lᵒᵈ

class TopologicalLattice (L : Type u_1) [TopologicalSpace L] [Lattice L] extends ContinuousInf L, ContinuousSup L : Prop

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.

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

instance OrderDual.topologicalLattice (L : Type u_1) [TopologicalSpace L] [Lattice L] [TopologicalLattice L] : TopologicalLattice Lᵒᵈ

@[instance 100]

instance LinearOrder.topologicalLattice {L : Type u_1} [TopologicalSpace L] [LinearOrder L] [OrderClosedTopology L] : TopologicalLattice L

theorem continuous_inf {L : Type u_1} [TopologicalSpace L] [Min 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] [Min L] [ContinuousInf L] {f g : X → L} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : X) => f x ⊓ g x

theorem continuous_sup {L : Type u_1} [TopologicalSpace L] [Max 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] [Max L] [ContinuousSup L] {f g : X → L} (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 g : α → L} {x y : L} [Max L] [ContinuousSup L] (hf : Tendsto f l (nhds x)) (hg : Tendsto g l (nhds y)) : Tendsto (f ⊔ g) l (nhds (x ⊔ y))

theorem Filter.Tendsto.sup_nhds {L : Type u_1} [TopologicalSpace L] {α : Type u_3} {l : Filter α} {f g : α → L} {x y : L} [Max L] [ContinuousSup L] (hf : Tendsto f l (nhds x)) (hg : Tendsto g l (nhds y)) : 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 g : α → L} {x y : L} [Min L] [ContinuousInf L] (hf : Tendsto f l (nhds x)) (hg : Tendsto g l (nhds y)) : Tendsto (f ⊓ g) l (nhds (x ⊓ y))

theorem Filter.Tendsto.inf_nhds {L : Type u_1} [TopologicalSpace L] {α : Type u_3} {l : Filter α} {f g : α → L} {x y : L} [Min L] [ContinuousInf L] (hf : Tendsto f l (nhds x)) (hg : Tendsto g l (nhds y)) : 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 : ∀ i ∈ s, Tendsto (f i) l (nhds (g i))) : 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 : ∀ i ∈ s, Tendsto (f i) l (nhds (g i))) : 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 : ∀ i ∈ s, Tendsto (f i) l (nhds (g i))) : 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 : ∀ i ∈ s, Tendsto (f i) l (nhds (g i))) : 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 : ∀ i ∈ s, Tendsto (f i) l (nhds (g i))) : 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 : ∀ i ∈ s, Tendsto (f i) l (nhds (g i))) : 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 : ∀ i ∈ s, Tendsto (f i) l (nhds (g i))) : 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 : ∀ i ∈ s, Tendsto (f i) l (nhds (g i))) : 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] [Max L] [ContinuousSup L] {f g : X → L} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (f ⊔ g) x

theorem ContinuousAt.sup {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Max L] [ContinuousSup L] {f g : X → L} {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] [Max L] [ContinuousSup L] {f g : X → L} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (f ⊔ g) s x

theorem ContinuousWithinAt.sup {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Max L] [ContinuousSup L] {f g : X → L} {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] [Max L] [ContinuousSup L] {f g : X → L} {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (f ⊔ g) s

theorem ContinuousOn.sup {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Max L] [ContinuousSup L] {f g : X → L} {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] [Max L] [ContinuousSup L] {f g : X → L} (hf : Continuous f) (hg : Continuous g) : Continuous (f ⊔ g)

theorem ContinuousAt.inf' {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Min L] [ContinuousInf L] {f g : X → L} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (f ⊓ g) x

theorem ContinuousAt.inf {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Min L] [ContinuousInf L] {f g : X → L} {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] [Min L] [ContinuousInf L] {f g : X → L} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (f ⊓ g) s x

theorem ContinuousWithinAt.inf {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Min L] [ContinuousInf L] {f g : X → L} {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] [Min L] [ContinuousInf L] {f g : X → L} {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (f ⊓ g) s

theorem ContinuousOn.inf {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Min L] [ContinuousInf L] {f g : X → L} {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] [Min L] [ContinuousInf L] {f g : X → L} (hf : Continuous f) (hg : Continuous g) : Continuous (f ⊓ 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 : ι → X → L} {x : X} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} {x : X} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} {x : X} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} {x : X} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} {x : X} (hs : ∀ i ∈ s, 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 : ι → X → L} {x : X} (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} {x : X} (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} {x : X} (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} (hs : ∀ i ∈ s, 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 : ι → X → L} (hs : ∀ i ∈ s, 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 : ι → X → L} (hs : ∀ i ∈ s, 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 : ι → X → L} {x : X} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} {x : X} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} {x : X} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} {x : X} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} (hne : s.Nonempty) (hs : ∀ i ∈ s, 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 : ι → X → L} {x : X} (hs : ∀ i ∈ s, 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 : ι → X → L} {x : X} (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} {x : X} (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} {x : X} (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} (hs : ∀ i ∈ s, 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 : ι → X → L} {t : Set X} (hs : ∀ i ∈ s, 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 : ι → X → L} (hs : ∀ i ∈ s, 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 : ι → X → L} (hs : ∀ i ∈ s, Continuous (f i)) : Continuous (s.inf f)