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

source
๐Ÿ”ถ coverage
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

Instances
    source
    ๐Ÿ”ถ coverage
    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

    Instances
      source
      ๐Ÿ“ coverage
      instance OrderDual.continuousSup (L : Type u_1) [TopologicalSpace L] [Min L] [h : ContinuousInf L] :
      ContinuousSup Lแต’แตˆ
      source
      ๐Ÿ“ coverage
      instance OrderDual.continuousInf (L : Type u_1) [TopologicalSpace L] [Max L] [h : ContinuousSup L] :
      ContinuousInf Lแต’แตˆ
      source
      ๐Ÿ”ถ coverage
      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.

      Instances
        source
        ๐Ÿ“ coverage
        instance OrderDual.topologicalLattice (L : Type u_1) [TopologicalSpace L] [Lattice L] [TopologicalLattice L] :
        TopologicalLattice Lแต’แตˆ
        source
        ๐Ÿ“ coverage
        @[instance 100]
        instance LinearOrder.topologicalLattice {L : Type u_1} [TopologicalSpace L] [LinearOrder L] [OrderClosedTopology L] :
        TopologicalLattice L
        source
        ๐Ÿ“ coverage
        theorem continuous_inf {L : Type u_1} [TopologicalSpace L] [Min L] [ContinuousInf L] :
        Continuous fun (p : L ร— L) => p.1 โŠ“ p.2
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        theorem continuous_sup {L : Type u_1} [TopologicalSpace L] [Max L] [ContinuousSup L] :
        Continuous fun (p : L ร— L) => p.1 โŠ” p.2
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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))
        source
        ๐Ÿ“ coverage
        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))
        source
        ๐Ÿ“ coverage
        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))
        source
        ๐Ÿ“ coverage
        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))
        source
        ๐Ÿ“ coverage
        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))
        source
        ๐Ÿ“ coverage
        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))
        source
        ๐Ÿ“ coverage
        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))
        source
        ๐Ÿ“ coverage
        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))
        source
        ๐Ÿ“ coverage
        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))
        source
        ๐Ÿ“ coverage
        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))
        source
        ๐Ÿ“ coverage
        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))
        source
        ๐Ÿ“ coverage
        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))
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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)
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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)
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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)
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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)
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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)
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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
        source
        ๐Ÿ“ coverage
        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)