Documentation

Mathlib.Topology.Semicontinuous

Semicontinuous maps #

A function f from a topological space α to an ordered space β is lower semicontinuous at a point x if, for any y < f x, for any x' close enough to x, one has f x' > y. In other words, f can jump up, but it can not jump down.

Upper semicontinuous functions are defined similarly.

This file introduces these notions, and a basic API around them mimicking the API for continuous functions.

Main definitions and results #

We introduce 4 definitions related to lower semicontinuity:

We build a basic API using dot notation around these notions, and we prove that

Similar results are stated and proved for upper semicontinuity.

We also prove that a function is continuous if and only if it is both lower and upper semicontinuous.

We have some equivalent definitions of lower- and upper-semicontinuity (under certain restrictions on the order on the codomain):

Implementation details #

All the nontrivial results for upper semicontinuous functions are deduced from the corresponding ones for lower semicontinuous functions using OrderDual.

References #

Main definitions #

def LowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : αβ) (s : Set α) (x : α) :

A real function f is lower semicontinuous at x within a set s if, for any ε > 0, for all x' close enough to x in s, then f x' is at least f x - ε. We formulate this in a general preordered space, using an arbitrary y < f x instead of f x - ε.

Equations
Instances For
    def LowerSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : αβ) (s : Set α) :

    A real function f is lower semicontinuous on a set s if, for any ε > 0, for any x ∈ s, for all x' close enough to x in s, then f x' is at least f x - ε. We formulate this in a general preordered space, using an arbitrary y < f x instead of f x - ε.

    Equations
    Instances For
      def LowerSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : αβ) (x : α) :

      A real function f is lower semicontinuous at x if, for any ε > 0, for all x' close enough to x, then f x' is at least f x - ε. We formulate this in a general preordered space, using an arbitrary y < f x instead of f x - ε.

      Equations
      Instances For
        def LowerSemicontinuous {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : αβ) :

        A real function f is lower semicontinuous if, for any ε > 0, for any x, for all x' close enough to x, then f x' is at least f x - ε. We formulate this in a general preordered space, using an arbitrary y < f x instead of f x - ε.

        Equations
        Instances For
          def UpperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : αβ) (s : Set α) (x : α) :

          A real function f is upper semicontinuous at x within a set s if, for any ε > 0, for all x' close enough to x in s, then f x' is at most f x + ε. We formulate this in a general preordered space, using an arbitrary y > f x instead of f x + ε.

          Equations
          Instances For
            def UpperSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : αβ) (s : Set α) :

            A real function f is upper semicontinuous on a set s if, for any ε > 0, for any x ∈ s, for all x' close enough to x in s, then f x' is at most f x + ε. We formulate this in a general preordered space, using an arbitrary y > f x instead of f x + ε.

            Equations
            Instances For
              def UpperSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : αβ) (x : α) :

              A real function f is upper semicontinuous at x if, for any ε > 0, for all x' close enough to x, then f x' is at most f x + ε. We formulate this in a general preordered space, using an arbitrary y > f x instead of f x + ε.

              Equations
              Instances For
                def UpperSemicontinuous {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : αβ) :

                A real function f is upper semicontinuous if, for any ε > 0, for any x, for all x' close enough to x, then f x' is at most f x + ε. We formulate this in a general preordered space, using an arbitrary y > f x instead of f x + ε.

                Equations
                Instances For

                  Lower semicontinuous functions #

                  Basic dot notation interface for lower semicontinuity #

                  theorem LowerSemicontinuousWithinAt.mono {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} {x : α} {s : Set α} {t : Set α} (h : LowerSemicontinuousWithinAt f s x) (hst : t s) :
                  theorem lowerSemicontinuousWithinAt_univ_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} {x : α} :
                  theorem LowerSemicontinuousAt.lowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} {x : α} (s : Set α) (h : LowerSemicontinuousAt f x) :
                  theorem LowerSemicontinuousOn.lowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} {x : α} {s : Set α} (h : LowerSemicontinuousOn f s) (hx : x s) :
                  theorem LowerSemicontinuousOn.mono {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} {s : Set α} {t : Set α} (h : LowerSemicontinuousOn f s) (hst : t s) :
                  theorem lowerSemicontinuousOn_univ_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} :
                  theorem LowerSemicontinuous.lowerSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} (h : LowerSemicontinuous f) (x : α) :
                  theorem LowerSemicontinuous.lowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} (h : LowerSemicontinuous f) (s : Set α) (x : α) :
                  theorem LowerSemicontinuous.lowerSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} (h : LowerSemicontinuous f) (s : Set α) :

                  Constants #

                  theorem lowerSemicontinuousWithinAt_const {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {x : α} {s : Set α} {z : β} :
                  LowerSemicontinuousWithinAt (fun (_x : α) => z) s x
                  theorem lowerSemicontinuousAt_const {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {x : α} {z : β} :
                  LowerSemicontinuousAt (fun (_x : α) => z) x
                  theorem lowerSemicontinuousOn_const {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {s : Set α} {z : β} :
                  LowerSemicontinuousOn (fun (_x : α) => z) s
                  theorem lowerSemicontinuous_const {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {z : β} :
                  LowerSemicontinuous fun (_x : α) => z

                  Indicators #

                  theorem IsOpen.lowerSemicontinuous_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {s : Set α} {y : β} [Zero β] (hs : IsOpen s) (hy : 0 y) :
                  LowerSemicontinuous (s.indicator fun (_x : α) => y)
                  theorem IsOpen.lowerSemicontinuousOn_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {s : Set α} {t : Set α} {y : β} [Zero β] (hs : IsOpen s) (hy : 0 y) :
                  LowerSemicontinuousOn (s.indicator fun (_x : α) => y) t
                  theorem IsOpen.lowerSemicontinuousAt_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {x : α} {s : Set α} {y : β} [Zero β] (hs : IsOpen s) (hy : 0 y) :
                  LowerSemicontinuousAt (s.indicator fun (_x : α) => y) x
                  theorem IsOpen.lowerSemicontinuousWithinAt_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {x : α} {s : Set α} {t : Set α} {y : β} [Zero β] (hs : IsOpen s) (hy : 0 y) :
                  LowerSemicontinuousWithinAt (s.indicator fun (_x : α) => y) t x
                  theorem IsClosed.lowerSemicontinuous_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {s : Set α} {y : β} [Zero β] (hs : IsClosed s) (hy : y 0) :
                  LowerSemicontinuous (s.indicator fun (_x : α) => y)
                  theorem IsClosed.lowerSemicontinuousOn_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {s : Set α} {t : Set α} {y : β} [Zero β] (hs : IsClosed s) (hy : y 0) :
                  LowerSemicontinuousOn (s.indicator fun (_x : α) => y) t
                  theorem IsClosed.lowerSemicontinuousAt_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {x : α} {s : Set α} {y : β} [Zero β] (hs : IsClosed s) (hy : y 0) :
                  LowerSemicontinuousAt (s.indicator fun (_x : α) => y) x
                  theorem IsClosed.lowerSemicontinuousWithinAt_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {x : α} {s : Set α} {t : Set α} {y : β} [Zero β] (hs : IsClosed s) (hy : y 0) :
                  LowerSemicontinuousWithinAt (s.indicator fun (_x : α) => y) t x

                  Relationship with continuity #

                  theorem lowerSemicontinuous_iff_isOpen_preimage {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} :
                  theorem LowerSemicontinuous.isOpen_preimage {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} (hf : LowerSemicontinuous f) (y : β) :
                  theorem lowerSemicontinuous_iff_isClosed_preimage {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] {f : αγ} :
                  theorem LowerSemicontinuous.isClosed_preimage {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] {f : αγ} (hf : LowerSemicontinuous f) (y : γ) :
                  theorem ContinuousWithinAt.lowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} (h : ContinuousWithinAt f s x) :
                  theorem ContinuousAt.lowerSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} (h : ContinuousAt f x) :
                  theorem ContinuousOn.lowerSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} (h : ContinuousOn f s) :

                  Equivalent definitions #

                  theorem lowerSemicontinuousWithinAt_iff_le_liminf {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :
                  theorem LowerSemicontinuousWithinAt.le_liminf {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :

                  Alias of the forward direction of lowerSemicontinuousWithinAt_iff_le_liminf.

                  theorem lowerSemicontinuousAt_iff_le_liminf {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :
                  theorem LowerSemicontinuousAt.le_liminf {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :

                  Alias of the forward direction of lowerSemicontinuousAt_iff_le_liminf.

                  theorem lowerSemicontinuous_iff_le_liminf {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :
                  LowerSemicontinuous f ∀ (x : α), f x Filter.liminf f (nhds x)
                  theorem LowerSemicontinuous.le_liminf {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :
                  LowerSemicontinuous f∀ (x : α), f x Filter.liminf f (nhds x)

                  Alias of the forward direction of lowerSemicontinuous_iff_le_liminf.

                  theorem lowerSemicontinuousOn_iff_le_liminf {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :
                  theorem LowerSemicontinuousOn.le_liminf {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :
                  LowerSemicontinuousOn f sxs, f x Filter.liminf f (nhdsWithin x s)

                  Alias of the forward direction of lowerSemicontinuousOn_iff_le_liminf.

                  @[deprecated lowerSemicontinuous_iff_isClosed_epigraph]
                  theorem lowerSemicontinuous_iff_IsClosed_epigraph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} :
                  LowerSemicontinuous f IsClosed {p : α × γ | f p.1 p.2}

                  Alias of lowerSemicontinuous_iff_isClosed_epigraph.

                  theorem LowerSemicontinuous.isClosed_epigraph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} :
                  LowerSemicontinuous fIsClosed {p : α × γ | f p.1 p.2}

                  Alias of the forward direction of lowerSemicontinuous_iff_isClosed_epigraph.

                  @[deprecated LowerSemicontinuous.isClosed_epigraph]
                  theorem LowerSemicontinuous.IsClosed_epigraph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} :
                  LowerSemicontinuous fIsClosed {p : α × γ | f p.1 p.2}

                  Alias of the forward direction of lowerSemicontinuous_iff_isClosed_epigraph.


                  Alias of the forward direction of lowerSemicontinuous_iff_isClosed_epigraph.

                  Composition #

                  theorem ContinuousAt.comp_lowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousWithinAt f s x) (gmon : Monotone g) :
                  theorem ContinuousAt.comp_lowerSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousAt f x) (gmon : Monotone g) :
                  theorem Continuous.comp_lowerSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : Continuous g) (hf : LowerSemicontinuousOn f s) (gmon : Monotone g) :
                  theorem Continuous.comp_lowerSemicontinuous {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : Continuous g) (hf : LowerSemicontinuous f) (gmon : Monotone g) :
                  theorem ContinuousAt.comp_lowerSemicontinuousWithinAt_antitone {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousWithinAt f s x) (gmon : Antitone g) :
                  theorem ContinuousAt.comp_lowerSemicontinuousAt_antitone {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousAt f x) (gmon : Antitone g) :
                  theorem Continuous.comp_lowerSemicontinuousOn_antitone {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : Continuous g) (hf : LowerSemicontinuousOn f s) (gmon : Antitone g) :
                  theorem Continuous.comp_lowerSemicontinuous_antitone {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : Continuous g) (hf : LowerSemicontinuous f) (gmon : Antitone g) :
                  theorem LowerSemicontinuousAt.comp_continuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : αβ} {g : ια} {x : ι} (hf : LowerSemicontinuousAt f (g x)) (hg : ContinuousAt g x) :
                  LowerSemicontinuousAt (fun (x : ι) => f (g x)) x
                  theorem LowerSemicontinuousAt.comp_continuousAt_of_eq {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : αβ} {g : ια} {y : α} {x : ι} (hf : LowerSemicontinuousAt f y) (hg : ContinuousAt g x) (hy : g x = y) :
                  LowerSemicontinuousAt (fun (x : ι) => f (g x)) x
                  theorem LowerSemicontinuous.comp_continuous {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : αβ} {g : ια} (hf : LowerSemicontinuous f) (hg : Continuous g) :
                  LowerSemicontinuous fun (x : ι) => f (g x)

                  Addition #

                  theorem LowerSemicontinuousWithinAt.add' {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} {g : αγ} (hf : LowerSemicontinuousWithinAt f s x) (hg : LowerSemicontinuousWithinAt g s x) (hcont : ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (f x, g x)) :
                  LowerSemicontinuousWithinAt (fun (z : α) => f z + g z) s x

                  The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an explicit continuity assumption on addition, for application to EReal. The unprimed version of the lemma uses [ContinuousAdd].

                  theorem LowerSemicontinuousAt.add' {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} {g : αγ} (hf : LowerSemicontinuousAt f x) (hg : LowerSemicontinuousAt g x) (hcont : ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (f x, g x)) :
                  LowerSemicontinuousAt (fun (z : α) => f z + g z) x

                  The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an explicit continuity assumption on addition, for application to EReal. The unprimed version of the lemma uses [ContinuousAdd].

                  theorem LowerSemicontinuousOn.add' {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} {g : αγ} (hf : LowerSemicontinuousOn f s) (hg : LowerSemicontinuousOn g s) (hcont : xs, ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (f x, g x)) :
                  LowerSemicontinuousOn (fun (z : α) => f z + g z) s

                  The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an explicit continuity assumption on addition, for application to EReal. The unprimed version of the lemma uses [ContinuousAdd].

                  theorem LowerSemicontinuous.add' {α : Type u_1} [TopologicalSpace α] {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} {g : αγ} (hf : LowerSemicontinuous f) (hg : LowerSemicontinuous g) (hcont : ∀ (x : α), ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (f x, g x)) :
                  LowerSemicontinuous fun (z : α) => f z + g z

                  The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an explicit continuity assumption on addition, for application to EReal. The unprimed version of the lemma uses [ContinuousAdd].

                  theorem LowerSemicontinuousWithinAt.add {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : αγ} {g : αγ} (hf : LowerSemicontinuousWithinAt f s x) (hg : LowerSemicontinuousWithinAt g s x) :
                  LowerSemicontinuousWithinAt (fun (z : α) => f z + g z) s x

                  The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with [ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on addition, for application to EReal.

                  theorem LowerSemicontinuousAt.add {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : αγ} {g : αγ} (hf : LowerSemicontinuousAt f x) (hg : LowerSemicontinuousAt g x) :
                  LowerSemicontinuousAt (fun (z : α) => f z + g z) x

                  The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with [ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on addition, for application to EReal.

                  theorem LowerSemicontinuousOn.add {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : αγ} {g : αγ} (hf : LowerSemicontinuousOn f s) (hg : LowerSemicontinuousOn g s) :
                  LowerSemicontinuousOn (fun (z : α) => f z + g z) s

                  The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with [ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on addition, for application to EReal.

                  theorem LowerSemicontinuous.add {α : Type u_1} [TopologicalSpace α] {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : αγ} {g : αγ} (hf : LowerSemicontinuous f) (hg : LowerSemicontinuous g) :
                  LowerSemicontinuous fun (z : α) => f z + g z

                  The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with [ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on addition, for application to EReal.

                  theorem lowerSemicontinuousWithinAt_sum {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Type u_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ιαγ} {a : Finset ι} (ha : ia, LowerSemicontinuousWithinAt (f i) s x) :
                  LowerSemicontinuousWithinAt (fun (z : α) => ia, f i z) s x
                  theorem lowerSemicontinuousAt_sum {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Type u_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ιαγ} {a : Finset ι} (ha : ia, LowerSemicontinuousAt (f i) x) :
                  LowerSemicontinuousAt (fun (z : α) => ia, f i z) x
                  theorem lowerSemicontinuousOn_sum {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Type u_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ιαγ} {a : Finset ι} (ha : ia, LowerSemicontinuousOn (f i) s) :
                  LowerSemicontinuousOn (fun (z : α) => ia, f i z) s
                  theorem lowerSemicontinuous_sum {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ιαγ} {a : Finset ι} (ha : ia, LowerSemicontinuous (f i)) :
                  LowerSemicontinuous fun (z : α) => ia, f i z

                  Supremum #

                  theorem lowerSemicontinuousWithinAt_ciSup {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ιαδ'} (bdd : ∀ᶠ (y : α) in nhdsWithin x s, BddAbove (Set.range fun (i : ι) => f i y)) (h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x) :
                  LowerSemicontinuousWithinAt (fun (x' : α) => ⨆ (i : ι), f i x') s x
                  theorem lowerSemicontinuousWithinAt_iSup {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {f : ιαδ} (h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x) :
                  LowerSemicontinuousWithinAt (fun (x' : α) => ⨆ (i : ι), f i x') s x
                  theorem lowerSemicontinuousWithinAt_biSup {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {p : ιProp} {f : (i : ι) → p iαδ} (h : ∀ (i : ι) (hi : p i), LowerSemicontinuousWithinAt (f i hi) s x) :
                  LowerSemicontinuousWithinAt (fun (x' : α) => ⨆ (i : ι), ⨆ (hi : p i), f i hi x') s x
                  theorem lowerSemicontinuousAt_ciSup {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ιαδ'} (bdd : ∀ᶠ (y : α) in nhds x, BddAbove (Set.range fun (i : ι) => f i y)) (h : ∀ (i : ι), LowerSemicontinuousAt (f i) x) :
                  LowerSemicontinuousAt (fun (x' : α) => ⨆ (i : ι), f i x') x
                  theorem lowerSemicontinuousAt_iSup {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {f : ιαδ} (h : ∀ (i : ι), LowerSemicontinuousAt (f i) x) :
                  LowerSemicontinuousAt (fun (x' : α) => ⨆ (i : ι), f i x') x
                  theorem lowerSemicontinuousAt_biSup {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {p : ιProp} {f : (i : ι) → p iαδ} (h : ∀ (i : ι) (hi : p i), LowerSemicontinuousAt (f i hi) x) :
                  LowerSemicontinuousAt (fun (x' : α) => ⨆ (i : ι), ⨆ (hi : p i), f i hi x') x
                  theorem lowerSemicontinuousOn_ciSup {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ιαδ'} (bdd : xs, BddAbove (Set.range fun (i : ι) => f i x)) (h : ∀ (i : ι), LowerSemicontinuousOn (f i) s) :
                  LowerSemicontinuousOn (fun (x' : α) => ⨆ (i : ι), f i x') s
                  theorem lowerSemicontinuousOn_iSup {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {f : ιαδ} (h : ∀ (i : ι), LowerSemicontinuousOn (f i) s) :
                  LowerSemicontinuousOn (fun (x' : α) => ⨆ (i : ι), f i x') s
                  theorem lowerSemicontinuousOn_biSup {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {p : ιProp} {f : (i : ι) → p iαδ} (h : ∀ (i : ι) (hi : p i), LowerSemicontinuousOn (f i hi) s) :
                  LowerSemicontinuousOn (fun (x' : α) => ⨆ (i : ι), ⨆ (hi : p i), f i hi x') s
                  theorem lowerSemicontinuous_ciSup {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ιαδ'} (bdd : ∀ (x : α), BddAbove (Set.range fun (i : ι) => f i x)) (h : ∀ (i : ι), LowerSemicontinuous (f i)) :
                  LowerSemicontinuous fun (x' : α) => ⨆ (i : ι), f i x'
                  theorem lowerSemicontinuous_iSup {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {f : ιαδ} (h : ∀ (i : ι), LowerSemicontinuous (f i)) :
                  LowerSemicontinuous fun (x' : α) => ⨆ (i : ι), f i x'
                  theorem lowerSemicontinuous_biSup {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {p : ιProp} {f : (i : ι) → p iαδ} (h : ∀ (i : ι) (hi : p i), LowerSemicontinuous (f i hi)) :
                  LowerSemicontinuous fun (x' : α) => ⨆ (i : ι), ⨆ (hi : p i), f i hi x'

                  Infinite sums #

                  theorem lowerSemicontinuousWithinAt_tsum {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Type u_3} {f : ιαENNReal} (h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x) :
                  LowerSemicontinuousWithinAt (fun (x' : α) => ∑' (i : ι), f i x') s x
                  theorem lowerSemicontinuousAt_tsum {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Type u_3} {f : ιαENNReal} (h : ∀ (i : ι), LowerSemicontinuousAt (f i) x) :
                  LowerSemicontinuousAt (fun (x' : α) => ∑' (i : ι), f i x') x
                  theorem lowerSemicontinuousOn_tsum {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Type u_3} {f : ιαENNReal} (h : ∀ (i : ι), LowerSemicontinuousOn (f i) s) :
                  LowerSemicontinuousOn (fun (x' : α) => ∑' (i : ι), f i x') s
                  theorem lowerSemicontinuous_tsum {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {f : ιαENNReal} (h : ∀ (i : ι), LowerSemicontinuous (f i)) :
                  LowerSemicontinuous fun (x' : α) => ∑' (i : ι), f i x'

                  Upper semicontinuous functions #

                  Basic dot notation interface for upper semicontinuity #

                  theorem UpperSemicontinuousWithinAt.mono {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} {x : α} {s : Set α} {t : Set α} (h : UpperSemicontinuousWithinAt f s x) (hst : t s) :
                  theorem upperSemicontinuousWithinAt_univ_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} {x : α} :
                  theorem UpperSemicontinuousAt.upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} {x : α} (s : Set α) (h : UpperSemicontinuousAt f x) :
                  theorem UpperSemicontinuousOn.upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} {x : α} {s : Set α} (h : UpperSemicontinuousOn f s) (hx : x s) :
                  theorem UpperSemicontinuousOn.mono {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} {s : Set α} {t : Set α} (h : UpperSemicontinuousOn f s) (hst : t s) :
                  theorem upperSemicontinuousOn_univ_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} :
                  theorem UpperSemicontinuous.upperSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} (h : UpperSemicontinuous f) (x : α) :
                  theorem UpperSemicontinuous.upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} (h : UpperSemicontinuous f) (s : Set α) (x : α) :
                  theorem UpperSemicontinuous.upperSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} (h : UpperSemicontinuous f) (s : Set α) :

                  Constants #

                  theorem upperSemicontinuousWithinAt_const {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {x : α} {s : Set α} {z : β} :
                  UpperSemicontinuousWithinAt (fun (_x : α) => z) s x
                  theorem upperSemicontinuousAt_const {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {x : α} {z : β} :
                  UpperSemicontinuousAt (fun (_x : α) => z) x
                  theorem upperSemicontinuousOn_const {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {s : Set α} {z : β} :
                  UpperSemicontinuousOn (fun (_x : α) => z) s
                  theorem upperSemicontinuous_const {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {z : β} :
                  UpperSemicontinuous fun (_x : α) => z

                  Indicators #

                  theorem IsOpen.upperSemicontinuous_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {s : Set α} {y : β} [Zero β] (hs : IsOpen s) (hy : y 0) :
                  UpperSemicontinuous (s.indicator fun (_x : α) => y)
                  theorem IsOpen.upperSemicontinuousOn_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {s : Set α} {t : Set α} {y : β} [Zero β] (hs : IsOpen s) (hy : y 0) :
                  UpperSemicontinuousOn (s.indicator fun (_x : α) => y) t
                  theorem IsOpen.upperSemicontinuousAt_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {x : α} {s : Set α} {y : β} [Zero β] (hs : IsOpen s) (hy : y 0) :
                  UpperSemicontinuousAt (s.indicator fun (_x : α) => y) x
                  theorem IsOpen.upperSemicontinuousWithinAt_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {x : α} {s : Set α} {t : Set α} {y : β} [Zero β] (hs : IsOpen s) (hy : y 0) :
                  UpperSemicontinuousWithinAt (s.indicator fun (_x : α) => y) t x
                  theorem IsClosed.upperSemicontinuous_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {s : Set α} {y : β} [Zero β] (hs : IsClosed s) (hy : 0 y) :
                  UpperSemicontinuous (s.indicator fun (_x : α) => y)
                  theorem IsClosed.upperSemicontinuousOn_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {s : Set α} {t : Set α} {y : β} [Zero β] (hs : IsClosed s) (hy : 0 y) :
                  UpperSemicontinuousOn (s.indicator fun (_x : α) => y) t
                  theorem IsClosed.upperSemicontinuousAt_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {x : α} {s : Set α} {y : β} [Zero β] (hs : IsClosed s) (hy : 0 y) :
                  UpperSemicontinuousAt (s.indicator fun (_x : α) => y) x
                  theorem IsClosed.upperSemicontinuousWithinAt_indicator {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {x : α} {s : Set α} {t : Set α} {y : β} [Zero β] (hs : IsClosed s) (hy : 0 y) :
                  UpperSemicontinuousWithinAt (s.indicator fun (_x : α) => y) t x

                  Relationship with continuity #

                  theorem upperSemicontinuous_iff_isOpen_preimage {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} :
                  theorem UpperSemicontinuous.isOpen_preimage {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : αβ} (hf : UpperSemicontinuous f) (y : β) :
                  theorem upperSemicontinuous_iff_isClosed_preimage {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] {f : αγ} :
                  theorem UpperSemicontinuous.isClosed_preimage {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] {f : αγ} (hf : UpperSemicontinuous f) (y : γ) :
                  theorem ContinuousWithinAt.upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} (h : ContinuousWithinAt f s x) :
                  theorem ContinuousAt.upperSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} (h : ContinuousAt f x) :
                  theorem ContinuousOn.upperSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} (h : ContinuousOn f s) :

                  Equivalent definitions #

                  theorem upperSemicontinuousWithinAt_iff_limsup_le {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :
                  theorem UpperSemicontinuousWithinAt.limsup_le {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :

                  Alias of the forward direction of upperSemicontinuousWithinAt_iff_limsup_le.

                  theorem upperSemicontinuousAt_iff_limsup_le {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :
                  theorem UpperSemicontinuousAt.limsup_le {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :

                  Alias of the forward direction of upperSemicontinuousAt_iff_limsup_le.

                  theorem upperSemicontinuous_iff_limsup_le {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :
                  UpperSemicontinuous f ∀ (x : α), Filter.limsup f (nhds x) f x
                  theorem UpperSemicontinuous.limsup_le {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :
                  UpperSemicontinuous f∀ (x : α), Filter.limsup f (nhds x) f x

                  Alias of the forward direction of upperSemicontinuous_iff_limsup_le.

                  theorem upperSemicontinuousOn_iff_limsup_le {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :
                  theorem UpperSemicontinuousOn.limsup_le {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : αγ} :
                  UpperSemicontinuousOn f sxs, Filter.limsup f (nhdsWithin x s) f x

                  Alias of the forward direction of upperSemicontinuousOn_iff_limsup_le.

                  theorem UpperSemicontinuous.IsClosed_hypograph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} :
                  UpperSemicontinuous fIsClosed {p : α × γ | p.2 f p.1}

                  Alias of the forward direction of upperSemicontinuous_iff_IsClosed_hypograph.

                  Composition #

                  theorem ContinuousAt.comp_upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousWithinAt f s x) (gmon : Monotone g) :
                  theorem ContinuousAt.comp_upperSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousAt f x) (gmon : Monotone g) :
                  theorem Continuous.comp_upperSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : Continuous g) (hf : UpperSemicontinuousOn f s) (gmon : Monotone g) :
                  theorem Continuous.comp_upperSemicontinuous {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : Continuous g) (hf : UpperSemicontinuous f) (gmon : Monotone g) :
                  theorem ContinuousAt.comp_upperSemicontinuousWithinAt_antitone {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousWithinAt f s x) (gmon : Antitone g) :
                  theorem ContinuousAt.comp_upperSemicontinuousAt_antitone {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousAt f x) (gmon : Antitone g) :
                  theorem Continuous.comp_upperSemicontinuousOn_antitone {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : Continuous g) (hf : UpperSemicontinuousOn f s) (gmon : Antitone g) :
                  theorem Continuous.comp_upperSemicontinuous_antitone {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γδ} {f : αγ} (hg : Continuous g) (hf : UpperSemicontinuous f) (gmon : Antitone g) :
                  theorem UpperSemicontinuousAt.comp_continuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : αβ} {g : ια} {x : ι} (hf : UpperSemicontinuousAt f (g x)) (hg : ContinuousAt g x) :
                  UpperSemicontinuousAt (fun (x : ι) => f (g x)) x
                  theorem UpperSemicontinuousAt.comp_continuousAt_of_eq {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : αβ} {g : ια} {y : α} {x : ι} (hf : UpperSemicontinuousAt f y) (hg : ContinuousAt g x) (hy : g x = y) :
                  UpperSemicontinuousAt (fun (x : ι) => f (g x)) x
                  theorem UpperSemicontinuous.comp_continuous {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : αβ} {g : ια} (hf : UpperSemicontinuous f) (hg : Continuous g) :
                  UpperSemicontinuous fun (x : ι) => f (g x)

                  Addition #

                  theorem UpperSemicontinuousWithinAt.add' {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} {g : αγ} (hf : UpperSemicontinuousWithinAt f s x) (hg : UpperSemicontinuousWithinAt g s x) (hcont : ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (f x, g x)) :
                  UpperSemicontinuousWithinAt (fun (z : α) => f z + g z) s x

                  The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an explicit continuity assumption on addition, for application to EReal. The unprimed version of the lemma uses [ContinuousAdd].

                  theorem UpperSemicontinuousAt.add' {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} {g : αγ} (hf : UpperSemicontinuousAt f x) (hg : UpperSemicontinuousAt g x) (hcont : ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (f x, g x)) :
                  UpperSemicontinuousAt (fun (z : α) => f z + g z) x

                  The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an explicit continuity assumption on addition, for application to EReal. The unprimed version of the lemma uses [ContinuousAdd].

                  theorem UpperSemicontinuousOn.add' {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} {g : αγ} (hf : UpperSemicontinuousOn f s) (hg : UpperSemicontinuousOn g s) (hcont : xs, ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (f x, g x)) :
                  UpperSemicontinuousOn (fun (z : α) => f z + g z) s

                  The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an explicit continuity assumption on addition, for application to EReal. The unprimed version of the lemma uses [ContinuousAdd].

                  theorem UpperSemicontinuous.add' {α : Type u_1} [TopologicalSpace α] {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] {f : αγ} {g : αγ} (hf : UpperSemicontinuous f) (hg : UpperSemicontinuous g) (hcont : ∀ (x : α), ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (f x, g x)) :
                  UpperSemicontinuous fun (z : α) => f z + g z

                  The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an explicit continuity assumption on addition, for application to EReal. The unprimed version of the lemma uses [ContinuousAdd].

                  theorem UpperSemicontinuousWithinAt.add {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : αγ} {g : αγ} (hf : UpperSemicontinuousWithinAt f s x) (hg : UpperSemicontinuousWithinAt g s x) :
                  UpperSemicontinuousWithinAt (fun (z : α) => f z + g z) s x

                  The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with [ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on addition, for application to EReal.

                  theorem UpperSemicontinuousAt.add {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : αγ} {g : αγ} (hf : UpperSemicontinuousAt f x) (hg : UpperSemicontinuousAt g x) :
                  UpperSemicontinuousAt (fun (z : α) => f z + g z) x

                  The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with [ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on addition, for application to EReal.

                  theorem UpperSemicontinuousOn.add {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : αγ} {g : αγ} (hf : UpperSemicontinuousOn f s) (hg : UpperSemicontinuousOn g s) :
                  UpperSemicontinuousOn (fun (z : α) => f z + g z) s

                  The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with [ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on addition, for application to EReal.

                  theorem UpperSemicontinuous.add {α : Type u_1} [TopologicalSpace α] {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : αγ} {g : αγ} (hf : UpperSemicontinuous f) (hg : UpperSemicontinuous g) :
                  UpperSemicontinuous fun (z : α) => f z + g z

                  The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with [ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on addition, for application to EReal.

                  theorem upperSemicontinuousWithinAt_sum {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Type u_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ιαγ} {a : Finset ι} (ha : ia, UpperSemicontinuousWithinAt (f i) s x) :
                  UpperSemicontinuousWithinAt (fun (z : α) => ia, f i z) s x
                  theorem upperSemicontinuousAt_sum {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Type u_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ιαγ} {a : Finset ι} (ha : ia, UpperSemicontinuousAt (f i) x) :
                  UpperSemicontinuousAt (fun (z : α) => ia, f i z) x
                  theorem upperSemicontinuousOn_sum {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Type u_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ιαγ} {a : Finset ι} (ha : ia, UpperSemicontinuousOn (f i) s) :
                  UpperSemicontinuousOn (fun (z : α) => ia, f i z) s
                  theorem upperSemicontinuous_sum {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ιαγ} {a : Finset ι} (ha : ia, UpperSemicontinuous (f i)) :
                  UpperSemicontinuous fun (z : α) => ia, f i z

                  Infimum #

                  theorem upperSemicontinuousWithinAt_ciInf {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ιαδ'} (bdd : ∀ᶠ (y : α) in nhdsWithin x s, BddBelow (Set.range fun (i : ι) => f i y)) (h : ∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x) :
                  UpperSemicontinuousWithinAt (fun (x' : α) => ⨅ (i : ι), f i x') s x
                  theorem upperSemicontinuousWithinAt_iInf {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {f : ιαδ} (h : ∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x) :
                  UpperSemicontinuousWithinAt (fun (x' : α) => ⨅ (i : ι), f i x') s x
                  theorem upperSemicontinuousWithinAt_biInf {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {p : ιProp} {f : (i : ι) → p iαδ} (h : ∀ (i : ι) (hi : p i), UpperSemicontinuousWithinAt (f i hi) s x) :
                  UpperSemicontinuousWithinAt (fun (x' : α) => ⨅ (i : ι), ⨅ (hi : p i), f i hi x') s x
                  theorem upperSemicontinuousAt_ciInf {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ιαδ'} (bdd : ∀ᶠ (y : α) in nhds x, BddBelow (Set.range fun (i : ι) => f i y)) (h : ∀ (i : ι), UpperSemicontinuousAt (f i) x) :
                  UpperSemicontinuousAt (fun (x' : α) => ⨅ (i : ι), f i x') x
                  theorem upperSemicontinuousAt_iInf {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {f : ιαδ} (h : ∀ (i : ι), UpperSemicontinuousAt (f i) x) :
                  UpperSemicontinuousAt (fun (x' : α) => ⨅ (i : ι), f i x') x
                  theorem upperSemicontinuousAt_biInf {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {p : ιProp} {f : (i : ι) → p iαδ} (h : ∀ (i : ι) (hi : p i), UpperSemicontinuousAt (f i hi) x) :
                  UpperSemicontinuousAt (fun (x' : α) => ⨅ (i : ι), ⨅ (hi : p i), f i hi x') x
                  theorem upperSemicontinuousOn_ciInf {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ιαδ'} (bdd : xs, BddBelow (Set.range fun (i : ι) => f i x)) (h : ∀ (i : ι), UpperSemicontinuousOn (f i) s) :
                  UpperSemicontinuousOn (fun (x' : α) => ⨅ (i : ι), f i x') s
                  theorem upperSemicontinuousOn_iInf {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {f : ιαδ} (h : ∀ (i : ι), UpperSemicontinuousOn (f i) s) :
                  UpperSemicontinuousOn (fun (x' : α) => ⨅ (i : ι), f i x') s
                  theorem upperSemicontinuousOn_biInf {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {p : ιProp} {f : (i : ι) → p iαδ} (h : ∀ (i : ι) (hi : p i), UpperSemicontinuousOn (f i hi) s) :
                  UpperSemicontinuousOn (fun (x' : α) => ⨅ (i : ι), ⨅ (hi : p i), f i hi x') s
                  theorem upperSemicontinuous_ciInf {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ιαδ'} (bdd : ∀ (x : α), BddBelow (Set.range fun (i : ι) => f i x)) (h : ∀ (i : ι), UpperSemicontinuous (f i)) :
                  UpperSemicontinuous fun (x' : α) => ⨅ (i : ι), f i x'
                  theorem upperSemicontinuous_iInf {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {f : ιαδ} (h : ∀ (i : ι), UpperSemicontinuous (f i)) :
                  UpperSemicontinuous fun (x' : α) => ⨅ (i : ι), f i x'
                  theorem upperSemicontinuous_biInf {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {p : ιProp} {f : (i : ι) → p iαδ} (h : ∀ (i : ι) (hi : p i), UpperSemicontinuous (f i hi)) :
                  UpperSemicontinuous fun (x' : α) => ⨅ (i : ι), ⨅ (hi : p i), f i hi x'