doc-next-gen

Mathlib.Topology.Semicontinuous

Module docstring

{"# 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: * LowerSemicontinuousWithinAt f s x * LowerSemicontinuousAt f x * LowerSemicontinuousOn f s * LowerSemicontinuous f

We build a basic API using dot notation around these notions, and we prove that * constant functions are lower semicontinuous; * indicator s (fun _ ↦ y) is lower semicontinuous when s is open and 0 ≤ y, or when s is closed and y ≤ 0; * continuous functions are lower semicontinuous; * left composition with a continuous monotone functions maps lower semicontinuous functions to lower semicontinuous functions. If the function is anti-monotone, it instead maps lower semicontinuous functions to upper semicontinuous functions; * right composition with continuous functions preserves lower and upper semicontinuity; * a sum of two (or finitely many) lower semicontinuous functions is lower semicontinuous; * a supremum of a family of lower semicontinuous functions is lower semicontinuous; * An infinite sum of ℝ≥0∞-valued lower semicontinuous functions is lower semicontinuous.

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): * lowerSemicontinuous_iff_isOpen_preimage in a linear order; * lowerSemicontinuous_iff_isClosed_preimage in a linear order; * lowerSemicontinuousAt_iff_le_liminf in a dense complete linear order; * lowerSemicontinuous_iff_isClosed_epigraph in a dense complete linear order with the order topology.

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 ","### Lower semicontinuous functions ","#### Basic dot notation interface for lower semicontinuity ","#### Constants ","#### Indicators ","#### Relationship with continuity ","#### Equivalent definitions ","### Composition ","#### Addition ","#### Supremum ","#### Infinite sums ","### Upper semicontinuous functions ","#### Basic dot notation interface for upper semicontinuity ","#### Constants ","#### Indicators ","#### Relationship with continuity ","#### Equivalent definitions ","### Composition ","#### Addition ","#### Infimum "}

LowerSemicontinuousWithinAt definition
(f : α → β) (s : Set α) (x : α)
Full source 
/-- 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 - ε`. -/
def LowerSemicontinuousWithinAt (f : α → β) (s : Set α) (x : α) :=
  ∀ y < f x, ∀ᶠ x' in 𝓝[s] x, y < f x'
Lower semicontinuity at a point within a set
Informal description
A function \( f : \alpha \to \beta \) is lower semicontinuous at a point \( x \in \alpha \) within a set \( s \subseteq \alpha \) if for every \( y < f(x) \), there exists a neighborhood of \( x \) relative to \( s \) such that for all \( x' \) in this neighborhood, \( y < f(x') \). This means that \( f \) does not have any sudden downward jumps at \( x \) when restricted to \( s \).
LowerSemicontinuousOn definition
(f : α → β) (s : Set α)
Full source 
/-- 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 - ε`. -/
def LowerSemicontinuousOn (f : α → β) (s : Set α) :=
  ∀ x ∈ s, LowerSemicontinuousWithinAt f s x
Lower semicontinuity on a set
Informal description
A function \( f : \alpha \to \beta \) is lower semicontinuous on a set \( s \subseteq \alpha \) if for every point \( x \in s \), the function \( f \) is lower semicontinuous at \( x \) within \( s \). This means that for every \( y < f(x) \), there exists a neighborhood of \( x \) relative to \( s \) such that for all \( x' \) in this neighborhood, \( y < f(x') \). In other words, \( f \) does not have any sudden downward jumps at any point in \( s \).
LowerSemicontinuousAt definition
(f : α → β) (x : α)
Full source 
/-- 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 - ε`. -/
def LowerSemicontinuousAt (f : α → β) (x : α) :=
  ∀ y < f x, ∀ᶠ x' in 𝓝 x, y < f x'
Lower semicontinuity at a point
Informal description
A function \( f : \alpha \to \beta \) is lower semicontinuous at a point \( x \in \alpha \) if for every \( y < f(x) \), there exists a neighborhood of \( x \) such that for all \( x' \) in this neighborhood, \( y < f(x') \). This means that \( f \) does not have any sudden downward jumps at \( x \).
LowerSemicontinuous definition
(f : α → β)
Full source 
/-- 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 - ε`. -/
def LowerSemicontinuous (f : α → β) :=
  ∀ x, LowerSemicontinuousAt f x
Lower semicontinuous function
Informal description
A function \( f : \alpha \to \beta \) is lower semicontinuous if for every point \( x \in \alpha \), the function \( f \) is lower semicontinuous at \( x \). This means that for every \( y < f(x) \), there exists a neighborhood of \( x \) such that for all \( x' \) in this neighborhood, \( y < f(x') \). In other words, \( f \) does not have any sudden downward jumps at any point in its domain.
UpperSemicontinuousWithinAt definition
(f : α → β) (s : Set α) (x : α)
Full source 
/-- 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 + ε`. -/
def UpperSemicontinuousWithinAt (f : α → β) (s : Set α) (x : α) :=
  ∀ y, f x < y → ∀ᶠ x' in 𝓝[s] x, f x' < y
Upper semicontinuity within a set at a point
Informal description
A function \( f : \alpha \to \beta \) is upper semicontinuous at a point \( x \in \alpha \) within a set \( s \subseteq \alpha \) if for every \( y > f(x) \), there exists a neighborhood of \( x \) in \( s \) such that for all \( x' \) in this neighborhood, \( f(x') < y \). This means that \( f \) does not have any sudden upward jumps at \( x \) when restricted to \( s \).
UpperSemicontinuousOn definition
(f : α → β) (s : Set α)
Full source 
/-- 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 + ε`. -/
def UpperSemicontinuousOn (f : α → β) (s : Set α) :=
  ∀ x ∈ s, UpperSemicontinuousWithinAt f s x
Upper semicontinuous function on a set
Informal description
A function \( f : \alpha \to \beta \) is upper semicontinuous on a set \( s \subseteq \alpha \) if for every point \( x \in s \), the function \( f \) is upper semicontinuous at \( x \) within \( s \). This means that for every \( y > f(x) \), there exists a neighborhood of \( x \) in \( s \) such that for all \( x' \) in this neighborhood, \( f(x') < y \). In other words, \( f \) does not have any sudden upward jumps at any point in \( s \).
UpperSemicontinuousAt definition
(f : α → β) (x : α)
Full source 
/-- 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 + ε`. -/
def UpperSemicontinuousAt (f : α → β) (x : α) :=
  ∀ y, f x < y → ∀ᶠ x' in 𝓝 x, f x' < y
Upper semicontinuous function at a point
Informal description
A function $f \colon \alpha \to \beta$ between a topological space $\alpha$ and a preordered space $\beta$ is called *upper semicontinuous at a point $x \in \alpha$* if for any $y > f(x)$, there exists a neighborhood of $x$ such that for all $x'$ in this neighborhood, $f(x') < y$. In other words, $f$ can jump down but not up at $x$.
UpperSemicontinuous definition
(f : α → β)
Full source 
/-- 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 + ε`. -/
def UpperSemicontinuous (f : α → β) :=
  ∀ x, UpperSemicontinuousAt f x
Upper semicontinuous function
Informal description
A function $f \colon \alpha \to \beta$ from a topological space $\alpha$ to a preordered space $\beta$ is called *upper semicontinuous* if for every point $x \in \alpha$ and any $y > f(x)$, there exists a neighborhood of $x$ such that for all $x'$ in this neighborhood, $f(x') < y$. In other words, $f$ can jump down but not up at any point in its domain.
LowerSemicontinuousWithinAt.mono theorem
(h : LowerSemicontinuousWithinAt f s x) (hst : t ⊆ s) : LowerSemicontinuousWithinAt f t x
Full source 
theorem LowerSemicontinuousWithinAt.mono (h : LowerSemicontinuousWithinAt f s x) (hst : t ⊆ s) :
    LowerSemicontinuousWithinAt f t x := fun y hy =>
  Filter.Eventually.filter_mono (nhdsWithin_mono _ hst) (h y hy)
Restriction Preserves Lower Semicontinuity Within a Set
Informal description
Let $f : \alpha \to \beta$ be a function from a topological space $\alpha$ to an ordered space $\beta$. If $f$ is lower semicontinuous at $x \in \alpha$ within a set $s \subseteq \alpha$, and $t \subseteq s$, then $f$ is also lower semicontinuous at $x$ within $t$.
lowerSemicontinuousWithinAt_univ_iff theorem
: LowerSemicontinuousWithinAt f univ x ↔ LowerSemicontinuousAt f x
Full source 
theorem lowerSemicontinuousWithinAt_univ_iff :
    LowerSemicontinuousWithinAtLowerSemicontinuousWithinAt f univ x ↔ LowerSemicontinuousAt f x := by
  simp [LowerSemicontinuousWithinAt, LowerSemicontinuousAt, nhdsWithin_univ]
Equivalence of Lower Semicontinuity within Universal Set and Global Lower Semicontinuity at a Point
Informal description
A function $f \colon \alpha \to \beta$ is lower semicontinuous at a point $x \in \alpha$ within the universal set $\text{univ}$ if and only if it is lower semicontinuous at $x$ in the whole space $\alpha$.
LowerSemicontinuousAt.lowerSemicontinuousWithinAt theorem
(s : Set α) (h : LowerSemicontinuousAt f x) : LowerSemicontinuousWithinAt f s x
Full source 
theorem LowerSemicontinuousAt.lowerSemicontinuousWithinAt (s : Set α)
    (h : LowerSemicontinuousAt f x) : LowerSemicontinuousWithinAt f s x := fun y hy =>
  Filter.Eventually.filter_mono nhdsWithin_le_nhds (h y hy)
Global lower semicontinuity implies local lower semicontinuity within any subset
Informal description
Let $f : \alpha \to \beta$ be a function between a topological space $\alpha$ and an ordered space $\beta$. If $f$ is lower semicontinuous at a point $x \in \alpha$, then for any subset $s \subseteq \alpha$, $f$ is lower semicontinuous at $x$ within $s$.
LowerSemicontinuousOn.lowerSemicontinuousWithinAt theorem
(h : LowerSemicontinuousOn f s) (hx : x ∈ s) : LowerSemicontinuousWithinAt f s x
Full source 
theorem LowerSemicontinuousOn.lowerSemicontinuousWithinAt (h : LowerSemicontinuousOn f s)
    (hx : x ∈ s) : LowerSemicontinuousWithinAt f s x :=
  h x hx
Lower semicontinuity on a set implies lower semicontinuity at a point within the set
Informal description
If a function $f \colon \alpha \to \beta$ is lower semicontinuous on a set $s \subseteq \alpha$ and $x \in s$, then $f$ is lower semicontinuous at $x$ within $s$.
LowerSemicontinuousOn.mono theorem
(h : LowerSemicontinuousOn f s) (hst : t ⊆ s) : LowerSemicontinuousOn f t
Full source 
theorem LowerSemicontinuousOn.mono (h : LowerSemicontinuousOn f s) (hst : t ⊆ s) :
    LowerSemicontinuousOn f t := fun x hx => (h x (hst hx)).mono hst
Restriction Preserves Lower Semicontinuity on Subsets
Informal description
Let $f : \alpha \to \beta$ be a function from a topological space $\alpha$ to an ordered space $\beta$. If $f$ is lower semicontinuous on a set $s \subseteq \alpha$, and $t \subseteq s$, then $f$ is also lower semicontinuous on $t$.
lowerSemicontinuousOn_univ_iff theorem
: LowerSemicontinuousOn f univ ↔ LowerSemicontinuous f
Full source 
theorem lowerSemicontinuousOn_univ_iff : LowerSemicontinuousOnLowerSemicontinuousOn f univ ↔ LowerSemicontinuous f := by
  simp [LowerSemicontinuousOn, LowerSemicontinuous, lowerSemicontinuousWithinAt_univ_iff]
Lower Semicontinuity on Universal Set Equivalence
Informal description
A function $f \colon \alpha \to \beta$ is lower semicontinuous on the universal set $\text{univ} \subseteq \alpha$ if and only if it is lower semicontinuous.
LowerSemicontinuous.lowerSemicontinuousAt theorem
(h : LowerSemicontinuous f) (x : α) : LowerSemicontinuousAt f x
Full source 
theorem LowerSemicontinuous.lowerSemicontinuousAt (h : LowerSemicontinuous f) (x : α) :
    LowerSemicontinuousAt f x :=
  h x
Global lower semicontinuity implies pointwise lower semicontinuity
Informal description
If a function $f : \alpha \to \beta$ is lower semicontinuous, then for every point $x \in \alpha$, the function $f$ is lower semicontinuous at $x$.
LowerSemicontinuous.lowerSemicontinuousWithinAt theorem
(h : LowerSemicontinuous f) (s : Set α) (x : α) : LowerSemicontinuousWithinAt f s x
Full source 
theorem LowerSemicontinuous.lowerSemicontinuousWithinAt (h : LowerSemicontinuous f) (s : Set α)
    (x : α) : LowerSemicontinuousWithinAt f s x :=
  (h x).lowerSemicontinuousWithinAt s
Global lower semicontinuity implies local lower semicontinuity within any subset
Informal description
Let $f \colon \alpha \to \beta$ be a lower semicontinuous function between a topological space $\alpha$ and an ordered space $\beta$. Then for any subset $s \subseteq \alpha$ and any point $x \in \alpha$, the function $f$ is lower semicontinuous at $x$ within $s$.
LowerSemicontinuous.lowerSemicontinuousOn theorem
(h : LowerSemicontinuous f) (s : Set α) : LowerSemicontinuousOn f s
Full source 
theorem LowerSemicontinuous.lowerSemicontinuousOn (h : LowerSemicontinuous f) (s : Set α) :
    LowerSemicontinuousOn f s := fun x _hx => h.lowerSemicontinuousWithinAt s x
Global lower semicontinuity implies lower semicontinuity on any subset
Informal description
If a function $f \colon \alpha \to \beta$ is lower semicontinuous, then for any subset $s \subseteq \alpha$, the restriction of $f$ to $s$ is lower semicontinuous on $s$.
lowerSemicontinuousWithinAt_const theorem
: LowerSemicontinuousWithinAt (fun _x => z) s x
Full source 
theorem lowerSemicontinuousWithinAt_const : LowerSemicontinuousWithinAt (fun _x => z) s x :=
  fun _y hy => Filter.Eventually.of_forall fun _x => hy
Lower Semicontinuity of Constant Functions Within a Set
Informal description
For any constant function \( f : \alpha \to \beta \) defined by \( f(x) = z \) for all \( x \in \alpha \), \( f \) is lower semicontinuous at every point \( x \in \alpha \) within any set \( s \subseteq \alpha \).
lowerSemicontinuousAt_const theorem
: LowerSemicontinuousAt (fun _x => z) x
Full source 
theorem lowerSemicontinuousAt_const : LowerSemicontinuousAt (fun _x => z) x := fun _y hy =>
  Filter.Eventually.of_forall fun _x => hy
Lower Semicontinuity of Constant Functions
Informal description
For any constant function \( f : \alpha \to \beta \) defined by \( f(x) = z \) for all \( x \in \alpha \), \( f \) is lower semicontinuous at every point \( x \in \alpha \).
lowerSemicontinuousOn_const theorem
: LowerSemicontinuousOn (fun _x => z) s
Full source 
theorem lowerSemicontinuousOn_const : LowerSemicontinuousOn (fun _x => z) s := fun _x _hx =>
  lowerSemicontinuousWithinAt_const
Lower Semicontinuity of Constant Functions on a Set
Informal description
For any constant function $f : \alpha \to \beta$ defined by $f(x) = z$ for all $x \in \alpha$, $f$ is lower semicontinuous on any set $s \subseteq \alpha$.
lowerSemicontinuous_const theorem
: LowerSemicontinuous fun _x : α => z
Full source 
theorem lowerSemicontinuous_const : LowerSemicontinuous fun _x : α => z := fun _x =>
  lowerSemicontinuousAt_const
Lower Semicontinuity of Constant Functions
Informal description
The constant function $f : \alpha \to \beta$ defined by $f(x) = z$ for all $x \in \alpha$ is lower semicontinuous.
IsOpen.lowerSemicontinuous_indicator theorem
(hs : IsOpen s) (hy : 0 ≤ y) : LowerSemicontinuous (indicator s fun _x => y)
Full source 
theorem IsOpen.lowerSemicontinuous_indicator (hs : IsOpen s) (hy : 0 ≤ y) :
    LowerSemicontinuous (indicator s fun _x => y) := by
  intro x z hz
  by_cases h : x ∈ s <;> simp [h] at hz
  · filter_upwards [hs.mem_nhds h]
    simp +contextual [hz]
  · refine Filter.Eventually.of_forall fun x' => ?_
    by_cases h' : x' ∈ s <;> simp [h', hz.trans_le hy, hz]
Lower semicontinuity of indicator function on open set with non-negative value
Informal description
Let $s$ be an open set in a topological space $\alpha$ and let $y$ be a non-negative element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is lower semicontinuous on $\alpha$.
IsOpen.lowerSemicontinuousOn_indicator theorem
(hs : IsOpen s) (hy : 0 ≤ y) : LowerSemicontinuousOn (indicator s fun _x => y) t
Full source 
theorem IsOpen.lowerSemicontinuousOn_indicator (hs : IsOpen s) (hy : 0 ≤ y) :
    LowerSemicontinuousOn (indicator s fun _x => y) t :=
  (hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousOn t
Lower semicontinuity of indicator function on open set with non-negative value, restricted to any subset
Informal description
Let $s$ be an open subset of a topological space $\alpha$ and let $y$ be a non-negative element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is lower semicontinuous on any subset $t \subseteq \alpha$.
IsOpen.lowerSemicontinuousAt_indicator theorem
(hs : IsOpen s) (hy : 0 ≤ y) : LowerSemicontinuousAt (indicator s fun _x => y) x
Full source 
theorem IsOpen.lowerSemicontinuousAt_indicator (hs : IsOpen s) (hy : 0 ≤ y) :
    LowerSemicontinuousAt (indicator s fun _x => y) x :=
  (hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousAt x
Lower semicontinuity at a point for indicator function on open set with non-negative value
Informal description
Let $s$ be an open subset of a topological space $\alpha$ and let $y$ be a non-negative element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is lower semicontinuous at every point $x \in \alpha$.
IsOpen.lowerSemicontinuousWithinAt_indicator theorem
(hs : IsOpen s) (hy : 0 ≤ y) : LowerSemicontinuousWithinAt (indicator s fun _x => y) t x
Full source 
theorem IsOpen.lowerSemicontinuousWithinAt_indicator (hs : IsOpen s) (hy : 0 ≤ y) :
    LowerSemicontinuousWithinAt (indicator s fun _x => y) t x :=
  (hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousWithinAt t x
Lower Semicontinuity Within a Set for Indicator Function on Open Set with Non-Negative Value
Informal description
Let $s$ be an open subset of a topological space $\alpha$ and let $y$ be a non-negative element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is lower semicontinuous at a point $x$ within any subset $t \subseteq \alpha$.
IsClosed.lowerSemicontinuous_indicator theorem
(hs : IsClosed s) (hy : y ≤ 0) : LowerSemicontinuous (indicator s fun _x => y)
Full source 
theorem IsClosed.lowerSemicontinuous_indicator (hs : IsClosed s) (hy : y ≤ 0) :
    LowerSemicontinuous (indicator s fun _x => y) := by
  intro x z hz
  by_cases h : x ∈ s <;> simp [h] at hz
  · refine Filter.Eventually.of_forall fun x' => ?_
    by_cases h' : x' ∈ s <;> simp [h', hz, hz.trans_le hy]
  · filter_upwards [hs.isOpen_compl.mem_nhds h]
    simp +contextual [hz]
Lower Semicontinuity of Indicator Function on Closed Set with Non-Positive Value
Informal description
Let $s$ be a closed subset of a topological space $\alpha$ and let $y$ be a non-positive element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is lower semicontinuous on $\alpha$.
IsClosed.lowerSemicontinuousOn_indicator theorem
(hs : IsClosed s) (hy : y ≤ 0) : LowerSemicontinuousOn (indicator s fun _x => y) t
Full source 
theorem IsClosed.lowerSemicontinuousOn_indicator (hs : IsClosed s) (hy : y ≤ 0) :
    LowerSemicontinuousOn (indicator s fun _x => y) t :=
  (hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousOn t
Lower Semicontinuity of Indicator Function on Closed Set with Non-Positive Value over Any Subset
Informal description
Let $s$ be a closed subset of a topological space $\alpha$ and let $y \leq 0$ be an element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is lower semicontinuous on any subset $t \subseteq \alpha$.
IsClosed.lowerSemicontinuousAt_indicator theorem
(hs : IsClosed s) (hy : y ≤ 0) : LowerSemicontinuousAt (indicator s fun _x => y) x
Full source 
theorem IsClosed.lowerSemicontinuousAt_indicator (hs : IsClosed s) (hy : y ≤ 0) :
    LowerSemicontinuousAt (indicator s fun _x => y) x :=
  (hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousAt x
Lower Semicontinuity at a Point for Indicator Function on Closed Set with Non-Positive Value
Informal description
Let $s$ be a closed subset of a topological space $\alpha$ and let $y \leq 0$ be an element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is lower semicontinuous at every point $x \in \alpha$.
IsClosed.lowerSemicontinuousWithinAt_indicator theorem
(hs : IsClosed s) (hy : y ≤ 0) : LowerSemicontinuousWithinAt (indicator s fun _x => y) t x
Full source 
theorem IsClosed.lowerSemicontinuousWithinAt_indicator (hs : IsClosed s) (hy : y ≤ 0) :
    LowerSemicontinuousWithinAt (indicator s fun _x => y) t x :=
  (hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousWithinAt t x
Lower Semicontinuity Within a Set for Indicator Function on Closed Set with Non-Positive Value
Informal description
Let $s$ be a closed subset of a topological space $\alpha$, and let $y \leq 0$ be an element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is lower semicontinuous at any point $x \in \alpha$ within any subset $t \subseteq \alpha$.
lowerSemicontinuous_iff_isOpen_preimage theorem
: LowerSemicontinuous f ↔ ∀ y, IsOpen (f ⁻¹' Ioi y)
Full source 
theorem lowerSemicontinuous_iff_isOpen_preimage :
    LowerSemicontinuousLowerSemicontinuous f ↔ ∀ y, IsOpen (f ⁻¹' Ioi y) :=
  ⟨fun H y => isOpen_iff_mem_nhds.2 fun x hx => H x y hx, fun H _x y y_lt =>
    IsOpen.mem_nhds (H y) y_lt⟩
Characterization of Lower Semicontinuity via Open Preimages
Informal description
A function $f : \alpha \to \beta$ is lower semicontinuous if and only if for every $y \in \beta$, the preimage $f^{-1}((y, \infty))$ is an open set in $\alpha$.
LowerSemicontinuous.isOpen_preimage theorem
(hf : LowerSemicontinuous f) (y : β) : IsOpen (f ⁻¹' Ioi y)
Full source 
theorem LowerSemicontinuous.isOpen_preimage (hf : LowerSemicontinuous f) (y : β) :
    IsOpen (f ⁻¹' Ioi y) :=
  lowerSemicontinuous_iff_isOpen_preimage.1 hf y
Openness of Preimages Under Lower Semicontinuous Functions
Informal description
Let $f : \alpha \to \beta$ be a lower semicontinuous function. Then for any $y \in \beta$, the preimage $f^{-1}((y, \infty))$ is an open set in $\alpha$.
lowerSemicontinuous_iff_isClosed_preimage theorem
{f : α → γ} : LowerSemicontinuous f ↔ ∀ y, IsClosed (f ⁻¹' Iic y)
Full source 
theorem lowerSemicontinuous_iff_isClosed_preimage {f : α → γ} :
    LowerSemicontinuousLowerSemicontinuous f ↔ ∀ y, IsClosed (f ⁻¹' Iic y) := by
  rw [lowerSemicontinuous_iff_isOpen_preimage]
  simp only [← isOpen_compl_iff, ← preimage_compl, compl_Iic]
Characterization of lower semicontinuity via closed preimages of lower intervals
Informal description
A function $f \colon \alpha \to \gamma$ is lower semicontinuous if and only if for every $y \in \gamma$, the preimage $f^{-1}((-\infty, y])$ is a closed subset of $\alpha$.
LowerSemicontinuous.isClosed_preimage theorem
{f : α → γ} (hf : LowerSemicontinuous f) (y : γ) : IsClosed (f ⁻¹' Iic y)
Full source 
theorem LowerSemicontinuous.isClosed_preimage {f : α → γ} (hf : LowerSemicontinuous f) (y : γ) :
    IsClosed (f ⁻¹' Iic y) :=
  lowerSemicontinuous_iff_isClosed_preimage.1 hf y
Closed Preimages of Lower Intervals under Lower Semicontinuous Functions
Informal description
Let $f \colon \alpha \to \gamma$ be a lower semicontinuous function. Then for any $y \in \gamma$, the preimage $f^{-1}((-\infty, y])$ is a closed subset of $\alpha$.
ContinuousWithinAt.lowerSemicontinuousWithinAt theorem
{f : α → γ} (h : ContinuousWithinAt f s x) : LowerSemicontinuousWithinAt f s x
Full source 
theorem ContinuousWithinAt.lowerSemicontinuousWithinAt {f : α → γ} (h : ContinuousWithinAt f s x) :
    LowerSemicontinuousWithinAt f s x := fun _y hy => h (Ioi_mem_nhds hy)
Continuity within a set implies lower semicontinuity within that set
Informal description
Let $f \colon \alpha \to \gamma$ be a function between topological spaces. If $f$ is continuous at $x \in \alpha$ within a set $s \subseteq \alpha$, then $f$ is lower semicontinuous at $x$ within $s$.
ContinuousAt.lowerSemicontinuousAt theorem
{f : α → γ} (h : ContinuousAt f x) : LowerSemicontinuousAt f x
Full source 
theorem ContinuousAt.lowerSemicontinuousAt {f : α → γ} (h : ContinuousAt f x) :
    LowerSemicontinuousAt f x := fun _y hy => h (Ioi_mem_nhds hy)
Continuity implies lower semicontinuity at a point
Informal description
Let $f : \alpha \to \gamma$ be a function between topological spaces. If $f$ is continuous at a point $x \in \alpha$, then $f$ is lower semicontinuous at $x$.
ContinuousOn.lowerSemicontinuousOn theorem
{f : α → γ} (h : ContinuousOn f s) : LowerSemicontinuousOn f s
Full source 
theorem ContinuousOn.lowerSemicontinuousOn {f : α → γ} (h : ContinuousOn f s) :
    LowerSemicontinuousOn f s := fun x hx => (h x hx).lowerSemicontinuousWithinAt
Continuous functions are lower semicontinuous on their domain
Informal description
Let $f \colon \alpha \to \gamma$ be a continuous function on a set $s \subseteq \alpha$, where $\alpha$ is a topological space and $\gamma$ is an ordered space. Then $f$ is lower semicontinuous on $s$, meaning that for every $x \in s$ and every $y < f(x)$, there exists a neighborhood of $x$ in $s$ such that $f(x') > y$ for all $x'$ in this neighborhood.
Continuous.lowerSemicontinuous theorem
{f : α → γ} (h : Continuous f) : LowerSemicontinuous f
Full source 
theorem Continuous.lowerSemicontinuous {f : α → γ} (h : Continuous f) : LowerSemicontinuous f :=
  fun _x => h.continuousAt.lowerSemicontinuousAt
Continuous functions are lower semicontinuous
Informal description
Let $f : \alpha \to \gamma$ be a continuous function between topological spaces. Then $f$ is lower semicontinuous, meaning that for every $x \in \alpha$ and every $y < f(x)$, there exists a neighborhood of $x$ such that for all $x'$ in this neighborhood, $y < f(x')$.
lowerSemicontinuousWithinAt_iff_le_liminf theorem
{f : α → γ} : LowerSemicontinuousWithinAt f s x ↔ f x ≤ liminf f (𝓝[s] x)
Full source 
theorem lowerSemicontinuousWithinAt_iff_le_liminf {f : α → γ} :
    LowerSemicontinuousWithinAtLowerSemicontinuousWithinAt f s x ↔ f x ≤ liminf f (𝓝[s] x) := by
  constructor
  · intro hf; unfold LowerSemicontinuousWithinAt at hf
    contrapose! hf
    obtain ⟨y, lty, ylt⟩ := exists_between hf; use y
    exact ⟨ylt, fun h => lty.not_le
      (le_liminf_of_le (by isBoundedDefault) (h.mono fun _ hx => le_of_lt hx))⟩
  exact fun hf y ylt => eventually_lt_of_lt_liminf (ylt.trans_le hf)
Characterization of Lower Semicontinuity via Limit Inferior: $f$ is lower semicontinuous at $x$ within $s$ if and only if $f(x) \leq \liminf_{x' \to x, x' \in s} f(x')$
Informal description
Let $f : \alpha \to \gamma$ be a function from a topological space $\alpha$ to a conditionally complete linear order $\gamma$. Then $f$ is lower semicontinuous at a point $x \in \alpha$ within a set $s \subseteq \alpha$ if and only if $f(x) \leq \liminf_{x' \to x, x' \in s} f(x')$, where the limit inferior is taken with respect to the neighborhood filter of $x$ restricted to $s$.
lowerSemicontinuousAt_iff_le_liminf theorem
{f : α → γ} : LowerSemicontinuousAt f x ↔ f x ≤ liminf f (𝓝 x)
Full source 
theorem lowerSemicontinuousAt_iff_le_liminf {f : α → γ} :
    LowerSemicontinuousAtLowerSemicontinuousAt f x ↔ f x ≤ liminf f (𝓝 x) := by
  rw [← lowerSemicontinuousWithinAt_univ_iff, lowerSemicontinuousWithinAt_iff_le_liminf,
    ← nhdsWithin_univ]
Characterization of Lower Semicontinuity at a Point via Limit Inferior
Informal description
Let $f \colon \alpha \to \gamma$ be a function from a topological space $\alpha$ to a conditionally complete linear order $\gamma$. Then $f$ is lower semicontinuous at a point $x \in \alpha$ if and only if $f(x) \leq \liminf_{x' \to x} f(x')$, where the limit inferior is taken with respect to the neighborhood filter of $x$.
lowerSemicontinuous_iff_le_liminf theorem
{f : α → γ} : LowerSemicontinuous f ↔ ∀ x, f x ≤ liminf f (𝓝 x)
Full source 
theorem lowerSemicontinuous_iff_le_liminf {f : α → γ} :
    LowerSemicontinuousLowerSemicontinuous f ↔ ∀ x, f x ≤ liminf f (𝓝 x) := by
  simp only [← lowerSemicontinuousAt_iff_le_liminf, LowerSemicontinuous]
Characterization of Lower Semicontinuity via Limit Inferior
Informal description
A function $f \colon \alpha \to \gamma$ is lower semicontinuous if and only if for every point $x \in \alpha$, the value $f(x)$ is less than or equal to the limit inferior of $f$ as the argument approaches $x$ in the neighborhood filter $\mathcal{N}(x)$. In other words, $f$ is lower semicontinuous precisely when at every point $x$, the function value does not exceed the smallest limit point of $f$ near $x$.
lowerSemicontinuousOn_iff_le_liminf theorem
{f : α → γ} : LowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ liminf f (𝓝[s] x)
Full source 
theorem lowerSemicontinuousOn_iff_le_liminf {f : α → γ} :
    LowerSemicontinuousOnLowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ liminf f (𝓝[s] x) := by
  simp only [← lowerSemicontinuousWithinAt_iff_le_liminf, LowerSemicontinuousOn]
Characterization of Lower Semicontinuity via Limit Inferior on a Set
Informal description
A function $f : \alpha \to \gamma$ is lower semicontinuous on a set $s \subseteq \alpha$ if and only if for every point $x \in s$, the value $f(x)$ is less than or equal to the limit inferior of $f$ as $x'$ approaches $x$ within $s$.
lowerSemicontinuous_iff_isClosed_epigraph theorem
{f : α → γ} : LowerSemicontinuous f ↔ IsClosed {p : α × γ | f p.1 ≤ p.2}
Full source 
theorem lowerSemicontinuous_iff_isClosed_epigraph {f : α → γ} :
    LowerSemicontinuousLowerSemicontinuous f ↔ IsClosed {p : α × γ | f p.1 ≤ p.2} := by
  constructor
  · rw [lowerSemicontinuous_iff_le_liminf, isClosed_iff_forall_filter]
    rintro hf ⟨x, y⟩ F F_ne h h'
    rw [nhds_prod_eq, le_prod] at h'
    calc f x ≤ liminf f (𝓝 x) := hf x
    _ ≤ liminf f (map Prod.fst F) := liminf_le_liminf_of_le h'.1
    _ = liminf (f ∘ Prod.fst) F := (Filter.liminf_comp _ _ _).symm
    _ ≤ liminf Prod.snd F := liminf_le_liminfliminf_le_liminf <| by
          simpa using (eventually_principal.2 fun (_ : α × γ) ↦ id).filter_mono h
    _ = y := h'.2.liminf_eq
  · rw [lowerSemicontinuous_iff_isClosed_preimage]
    exact fun hf y ↦ hf.preimage (.prodMk_left y)
Characterization of Lower Semicontinuity via Closed Epigraph
Informal description
A function $f \colon \alpha \to \gamma$ is lower semicontinuous if and only if its epigraph $\{(x,y) \in \alpha \times \gamma \mid f(x) \leq y\}$ is a closed subset of $\alpha \times \gamma$.
ContinuousAt.comp_lowerSemicontinuousWithinAt theorem
{g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousWithinAt f s x) (gmon : Monotone g) : LowerSemicontinuousWithinAt (g ∘ f) s x
Full source 
theorem ContinuousAt.comp_lowerSemicontinuousWithinAt {g : γ → δ} {f : α → γ}
    (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousWithinAt f s x) (gmon : Monotone g) :
    LowerSemicontinuousWithinAt (g ∘ f) s x := by
  intro y hy
  by_cases h : ∃ l, l < f x
  · obtain ⟨z, zlt, hz⟩ : ∃ z < f x, Ioc z (f x) ⊆ g ⁻¹' Ioi y :=
      exists_Ioc_subset_of_mem_nhds (hg (Ioi_mem_nhds hy)) h
    filter_upwards [hf z zlt] with a ha
    calc
      y < g (min (f x) (f a)) := hz (by simp [zlt, ha, le_refl])
      _ ≤ g (f a) := gmon (min_le_right _ _)

  · simp only [not_exists, not_lt] at h
    exact Filter.Eventually.of_forall fun a => hy.trans_le (gmon (h (f a)))
Monotone Continuous Composition Preserves Lower Semicontinuity Within a Set
Informal description
Let $f \colon \alpha \to \gamma$ be a function that is lower semicontinuous at a point $x$ within a set $s \subseteq \alpha$, and let $g \colon \gamma \to \delta$ be a continuous function at $f(x)$. If $g$ is monotone, then the composition $g \circ f$ is lower semicontinuous at $x$ within $s$.
ContinuousAt.comp_lowerSemicontinuousAt theorem
{g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousAt f x) (gmon : Monotone g) : LowerSemicontinuousAt (g ∘ f) x
Full source 
theorem ContinuousAt.comp_lowerSemicontinuousAt {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x))
    (hf : LowerSemicontinuousAt f x) (gmon : Monotone g) : LowerSemicontinuousAt (g ∘ f) x := by
  simp only [← lowerSemicontinuousWithinAt_univ_iff] at hf ⊢
  exact hg.comp_lowerSemicontinuousWithinAt hf gmon
Monotone Continuous Composition Preserves Lower Semicontinuity at a Point
Informal description
Let $f \colon \alpha \to \gamma$ be a function that is lower semicontinuous at a point $x \in \alpha$, and let $g \colon \gamma \to \delta$ be a continuous function at $f(x)$. If $g$ is monotone, then the composition $g \circ f$ is lower semicontinuous at $x$.
Continuous.comp_lowerSemicontinuousOn theorem
{g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : LowerSemicontinuousOn f s) (gmon : Monotone g) : LowerSemicontinuousOn (g ∘ f) s
Full source 
theorem Continuous.comp_lowerSemicontinuousOn {g : γ → δ} {f : α → γ} (hg : Continuous g)
    (hf : LowerSemicontinuousOn f s) (gmon : Monotone g) : LowerSemicontinuousOn (g ∘ f) s :=
  fun x hx => hg.continuousAt.comp_lowerSemicontinuousWithinAt (hf x hx) gmon
Monotone Continuous Composition Preserves Lower Semicontinuity on a Set
Informal description
Let $f \colon \alpha \to \gamma$ be a lower semicontinuous function on a set $s \subseteq \alpha$, and let $g \colon \gamma \to \delta$ be a continuous function. If $g$ is monotone, then the composition $g \circ f$ is lower semicontinuous on $s$.
Continuous.comp_lowerSemicontinuous theorem
{g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : LowerSemicontinuous f) (gmon : Monotone g) : LowerSemicontinuous (g ∘ f)
Full source 
theorem Continuous.comp_lowerSemicontinuous {g : γ → δ} {f : α → γ} (hg : Continuous g)
    (hf : LowerSemicontinuous f) (gmon : Monotone g) : LowerSemicontinuous (g ∘ f) := fun x =>
  hg.continuousAt.comp_lowerSemicontinuousAt (hf x) gmon
Monotone Continuous Composition Preserves Lower Semicontinuity
Informal description
Let $f \colon \alpha \to \gamma$ be a lower semicontinuous function and $g \colon \gamma \to \delta$ be a continuous function. If $g$ is monotone, then the composition $g \circ f$ is lower semicontinuous.
ContinuousAt.comp_lowerSemicontinuousWithinAt_antitone theorem
{g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousWithinAt f s x) (gmon : Antitone g) : UpperSemicontinuousWithinAt (g ∘ f) s x
Full source 
theorem ContinuousAt.comp_lowerSemicontinuousWithinAt_antitone {g : γ → δ} {f : α → γ}
    (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousWithinAt f s x) (gmon : Antitone g) :
    UpperSemicontinuousWithinAt (g ∘ f) s x :=
  @ContinuousAt.comp_lowerSemicontinuousWithinAt α _ x s γ _ _ _ δᵒᵈ _ _ _ g f hg hf gmon
Antitone Continuous Composition Transforms Lower to Upper Semicontinuity Within a Set
Informal description
Let $f \colon \alpha \to \gamma$ be a function that is lower semicontinuous at a point $x$ within a set $s \subseteq \alpha$, and let $g \colon \gamma \to \delta$ be a function that is continuous at $f(x)$. If $g$ is antitone (order-reversing), then the composition $g \circ f$ is upper semicontinuous at $x$ within $s$.
ContinuousAt.comp_lowerSemicontinuousAt_antitone theorem
{g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousAt f x) (gmon : Antitone g) : UpperSemicontinuousAt (g ∘ f) x
Full source 
theorem ContinuousAt.comp_lowerSemicontinuousAt_antitone {g : γ → δ} {f : α → γ}
    (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousAt f x) (gmon : Antitone g) :
    UpperSemicontinuousAt (g ∘ f) x :=
  @ContinuousAt.comp_lowerSemicontinuousAt α _ x γ _ _ _ δᵒᵈ _ _ _ g f hg hf gmon
Antitone Continuous Composition Transforms Lower to Upper Semicontinuity at a Point
Informal description
Let $f \colon \alpha \to \gamma$ be a function that is lower semicontinuous at a point $x \in \alpha$, and let $g \colon \gamma \to \delta$ be a function that is continuous at $f(x)$. If $g$ is antitone (order-reversing), then the composition $g \circ f$ is upper semicontinuous at $x$.
Continuous.comp_lowerSemicontinuousOn_antitone theorem
{g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : LowerSemicontinuousOn f s) (gmon : Antitone g) : UpperSemicontinuousOn (g ∘ f) s
Full source 
theorem Continuous.comp_lowerSemicontinuousOn_antitone {g : γ → δ} {f : α → γ} (hg : Continuous g)
    (hf : LowerSemicontinuousOn f s) (gmon : Antitone g) : UpperSemicontinuousOn (g ∘ f) s :=
  fun x hx => hg.continuousAt.comp_lowerSemicontinuousWithinAt_antitone (hf x hx) gmon
Antitone Continuous Composition Transforms Lower to Upper Semicontinuity on a Set
Informal description
Let $f \colon \alpha \to \gamma$ be a function that is lower semicontinuous on a set $s \subseteq \alpha$, and let $g \colon \gamma \to \delta$ be a continuous function. If $g$ is antitone (order-reversing), then the composition $g \circ f$ is upper semicontinuous on $s$.
Continuous.comp_lowerSemicontinuous_antitone theorem
{g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : LowerSemicontinuous f) (gmon : Antitone g) : UpperSemicontinuous (g ∘ f)
Full source 
theorem Continuous.comp_lowerSemicontinuous_antitone {g : γ → δ} {f : α → γ} (hg : Continuous g)
    (hf : LowerSemicontinuous f) (gmon : Antitone g) : UpperSemicontinuous (g ∘ f) := fun x =>
  hg.continuousAt.comp_lowerSemicontinuousAt_antitone (hf x) gmon
Antitone Continuous Composition Transforms Lower to Upper Semicontinuous Functions
Informal description
Let $f \colon \alpha \to \gamma$ be a lower semicontinuous function, and let $g \colon \gamma \to \delta$ be a continuous function. If $g$ is antitone (i.e., order-reversing), then the composition $g \circ f$ is upper semicontinuous.
LowerSemicontinuousAt.comp_continuousAt theorem
{f : α → β} {g : ι → α} {x : ι} (hf : LowerSemicontinuousAt f (g x)) (hg : ContinuousAt g x) : LowerSemicontinuousAt (fun x ↦ f (g x)) x
Full source 
theorem LowerSemicontinuousAt.comp_continuousAt {f : α → β} {g : ι → α} {x : ι}
    (hf : LowerSemicontinuousAt f (g x)) (hg : ContinuousAt g x) :
    LowerSemicontinuousAt (fun x ↦ f (g x)) x :=
  fun _ lt ↦ hg.eventually (hf _ lt)
Composition of a Lower Semicontinuous Function with a Continuous Function Preserves Lower Semicontinuity at a Point
Informal description
Let $f : \alpha \to \beta$ be a function that is lower semicontinuous at $g(x)$, and let $g : \iota \to \alpha$ be a function that is continuous at $x$. Then the composition $f \circ g$ is lower semicontinuous at $x$.
LowerSemicontinuousAt.comp_continuousAt_of_eq theorem
{f : α → β} {g : ι → α} {y : α} {x : ι} (hf : LowerSemicontinuousAt f y) (hg : ContinuousAt g x) (hy : g x = y) : LowerSemicontinuousAt (fun x ↦ f (g x)) x
Full source 
theorem LowerSemicontinuousAt.comp_continuousAt_of_eq {f : α → β} {g : ι → α} {y : α} {x : ι}
    (hf : LowerSemicontinuousAt f y) (hg : ContinuousAt g x) (hy : g x = y) :
    LowerSemicontinuousAt (fun x ↦ f (g x)) x := by
  rw [← hy] at hf
  exact comp_continuousAt hf hg
Composition of Lower Semicontinuous Function with Continuous Function Preserves Lower Semicontinuity at Equal Points
Informal description
Let $f : \alpha \to \beta$ be a function that is lower semicontinuous at a point $y \in \alpha$, and let $g : \iota \to \alpha$ be a function that is continuous at a point $x \in \iota$ with $g(x) = y$. Then the composition $f \circ g$ is lower semicontinuous at $x$.
LowerSemicontinuous.comp_continuous theorem
{f : α → β} {g : ι → α} (hf : LowerSemicontinuous f) (hg : Continuous g) : LowerSemicontinuous fun x ↦ f (g x)
Full source 
theorem LowerSemicontinuous.comp_continuous {f : α → β} {g : ι → α}
    (hf : LowerSemicontinuous f) (hg : Continuous g) : LowerSemicontinuous fun x ↦ f (g x) :=
  fun x ↦ (hf (g x)).comp_continuousAt hg.continuousAt
Composition of Lower Semicontinuous and Continuous Functions is Lower Semicontinuous
Informal description
Let $f : \alpha \to \beta$ be a lower semicontinuous function and $g : \iota \to \alpha$ be a continuous function. Then the composition $f \circ g$ is lower semicontinuous.
LowerSemicontinuousWithinAt.add' theorem
{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
Full source 
/-- 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' {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 := by
  intro y hy
  obtain ⟨u, v, u_open, xu, v_open, xv, h⟩ :
    ∃ u v : Set γ,
      IsOpen u ∧ f x ∈ u ∧ IsOpen v ∧ g x ∈ v ∧ u ×ˢ v ⊆ { p : γ × γ | y < p.fst + p.snd } :=
    mem_nhds_prod_iff'.1 (hcont (isOpen_Ioi.mem_nhds hy))
  by_cases hx₁ : ∃ l, l < f x
  · obtain ⟨z₁, z₁lt, h₁⟩ : ∃ z₁ < f x, Ioc z₁ (f x) ⊆ u :=
      exists_Ioc_subset_of_mem_nhds (u_open.mem_nhds xu) hx₁
    by_cases hx₂ : ∃ l, l < g x
    · obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v :=
        exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂
      filter_upwards [hf z₁ z₁lt, hg z₂ z₂lt] with z h₁z h₂z
      have A1 : minmin (f z) (f x) ∈ u := by
        by_cases H : f z ≤ f x
        · simpa [H] using h₁ ⟨h₁z, H⟩
        · simpa [le_of_not_le H]
      have A2 : minmin (g z) (g x) ∈ v := by
        by_cases H : g z ≤ g x
        · simpa [H] using h₂ ⟨h₂z, H⟩
        · simpa [le_of_not_le H]
      have : (min (f z) (f x), min (g z) (g x))(min (f z) (f x), min (g z) (g x)) ∈ u ×ˢ v := ⟨A1, A2⟩
      calc
        y < min (f z) (f x) + min (g z) (g x) := h this
        _ ≤ f z + g z := add_le_add (min_le_left _ _) (min_le_left _ _)

    · simp only [not_exists, not_lt] at hx₂
      filter_upwards [hf z₁ z₁lt] with z h₁z
      have A1 : minmin (f z) (f x) ∈ u := by
        by_cases H : f z ≤ f x
        · simpa [H] using h₁ ⟨h₁z, H⟩
        · simpa [le_of_not_le H]
      have : (min (f z) (f x), g x)(min (f z) (f x), g x) ∈ u ×ˢ v := ⟨A1, xv⟩
      calc
        y < min (f z) (f x) + g x := h this
        _ ≤ f z + g z := add_le_add (min_le_left _ _) (hx₂ (g z))

  · simp only [not_exists, not_lt] at hx₁
    by_cases hx₂ : ∃ l, l < g x
    · obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v :=
        exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂
      filter_upwards [hg z₂ z₂lt] with z h₂z
      have A2 : minmin (g z) (g x) ∈ v := by
        by_cases H : g z ≤ g x
        · simpa [H] using h₂ ⟨h₂z, H⟩
        · simpa [le_of_not_le H] using h₂ ⟨z₂lt, le_rfl⟩
      have : (f x, min (g z) (g x))(f x, min (g z) (g x)) ∈ u ×ˢ v := ⟨xu, A2⟩
      calc
        y < f x + min (g z) (g x) := h this
        _ ≤ f z + g z := add_le_add (hx₁ (f z)) (min_le_left _ _)
    · simp only [not_exists, not_lt] at hx₁ hx₂
      apply Filter.Eventually.of_forall
      intro z
      have : (f x, g x)(f x, g x) ∈ u ×ˢ v := ⟨xu, xv⟩
      calc
        y < f x + g x := h this
        _ ≤ f z + g z := add_le_add (hx₁ (f z)) (hx₂ (g z))
Sum of Lower Semicontinuous Functions is Lower Semicontinuous (with Continuity Condition)
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two functions $f, g : \alpha \to \gamma$ that are lower semicontinuous at a point $x$ within a set $s \subseteq \alpha$, and assuming that the addition operation $+ : \gamma \times \gamma \to \gamma$ is continuous at the point $(f(x), g(x))$, then the sum $f + g$ is also lower semicontinuous at $x$ within $s$.
LowerSemicontinuousAt.add' theorem
{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
Full source 
/-- 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' {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 := by
  simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  exact hf.add' hg hcont
Sum of Lower Semicontinuous Functions at a Point is Lower Semicontinuous (with Continuity Condition)
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two functions $f, g : \alpha \to \gamma$ that are lower semicontinuous at a point $x \in \alpha$, and assuming that the addition operation $+ : \gamma \times \gamma \to \gamma$ is continuous at the point $(f(x), g(x))$, then the sum $f + g$ is also lower semicontinuous at $x$.
LowerSemicontinuousOn.add' theorem
{f g : α → γ} (hf : LowerSemicontinuousOn f s) (hg : LowerSemicontinuousOn g s) (hcont : ∀ x ∈ s, ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) : LowerSemicontinuousOn (fun z => f z + g z) s
Full source 
/-- 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' {f g : α → γ} (hf : LowerSemicontinuousOn f s)
    (hg : LowerSemicontinuousOn g s)
    (hcont : ∀ x ∈ s, ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) :
    LowerSemicontinuousOn (fun z => f z + g z) s := fun x hx =>
  (hf x hx).add' (hg x hx) (hcont x hx)
Sum of Lower Semicontinuous Functions is Lower Semicontinuous (with Continuity Condition) on a Set
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two functions $f, g : \alpha \to \gamma$ that are lower semicontinuous on a set $s \subseteq \alpha$, and assuming that for every $x \in s$, the addition operation $+ : \gamma \times \gamma \to \gamma$ is continuous at $(f(x), g(x))$, then the sum $f + g$ is also lower semicontinuous on $s$.
LowerSemicontinuous.add' theorem
{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
Full source 
/-- 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' {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 := fun x => (hf x).add' (hg x) (hcont x)
Sum of Lower Semicontinuous Functions is Lower Semicontinuous (with Continuity Condition)
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two lower semicontinuous functions $f, g : \alpha \to \gamma$ such that for every $x \in \alpha$, the addition operation $+ : \gamma \times \gamma \to \gamma$ is continuous at $(f(x), g(x))$, then the sum $f + g$ is also lower semicontinuous.
LowerSemicontinuousWithinAt.add theorem
{f g : α → γ} (hf : LowerSemicontinuousWithinAt f s x) (hg : LowerSemicontinuousWithinAt g s x) : LowerSemicontinuousWithinAt (fun z => f z + g z) s x
Full source 
/-- 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.add {f g : α → γ} (hf : LowerSemicontinuousWithinAt f s x)
    (hg : LowerSemicontinuousWithinAt g s x) :
    LowerSemicontinuousWithinAt (fun z => f z + g z) s x :=
  hf.add' hg continuous_add.continuousAt
Sum of Lower Semicontinuous Functions is Lower Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two functions $f, g : \alpha \to \gamma$ that are lower semicontinuous at a point $x$ within a set $s \subseteq \alpha$, then the sum $f + g$ is also lower semicontinuous at $x$ within $s$.
LowerSemicontinuousAt.add theorem
{f g : α → γ} (hf : LowerSemicontinuousAt f x) (hg : LowerSemicontinuousAt g x) : LowerSemicontinuousAt (fun z => f z + g z) x
Full source 
/-- 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 {f g : α → γ} (hf : LowerSemicontinuousAt f x)
    (hg : LowerSemicontinuousAt g x) : LowerSemicontinuousAt (fun z => f z + g z) x :=
  hf.add' hg continuous_add.continuousAt
Sum of Lower Semicontinuous Functions at a Point is Lower Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two functions $f, g : \alpha \to \gamma$ that are lower semicontinuous at a point $x \in \alpha$, then the sum $f + g$ is also lower semicontinuous at $x$.
LowerSemicontinuousOn.add theorem
{f g : α → γ} (hf : LowerSemicontinuousOn f s) (hg : LowerSemicontinuousOn g s) : LowerSemicontinuousOn (fun z => f z + g z) s
Full source 
/-- 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 {f g : α → γ} (hf : LowerSemicontinuousOn f s)
    (hg : LowerSemicontinuousOn g s) : LowerSemicontinuousOn (fun z => f z + g z) s :=
  hf.add' hg fun _x _hx => continuous_add.continuousAt
Sum of Lower Semicontinuous Functions is Lower Semicontinuous on a Set
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two functions $f, g : \alpha \to \gamma$ that are lower semicontinuous on a set $s \subseteq \alpha$, then the sum $f + g$ is also lower semicontinuous on $s$.
LowerSemicontinuous.add theorem
{f g : α → γ} (hf : LowerSemicontinuous f) (hg : LowerSemicontinuous g) : LowerSemicontinuous fun z => f z + g z
Full source 
/-- 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 {f g : α → γ} (hf : LowerSemicontinuous f)
    (hg : LowerSemicontinuous g) : LowerSemicontinuous fun z => f z + g z :=
  hf.add' hg fun _x => continuous_add.continuousAt
Sum of Lower Semicontinuous Functions is Lower Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. If $f, g : \alpha \to \gamma$ are lower semicontinuous functions, then their sum $f + g$ is also lower semicontinuous.
lowerSemicontinuousWithinAt_sum theorem
{f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) s x) : LowerSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x
Full source 
theorem lowerSemicontinuousWithinAt_sum {f : ι → α → γ} {a : Finset ι}
    (ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) s x) :
    LowerSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x := by
  classical
    induction a using Finset.induction_on with
    | empty => exact lowerSemicontinuousWithinAt_const
    | insert _ _ ia IH =>
      simp only [ia, Finset.sum_insert, not_false_iff]
      exact
        LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
          (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))
Finite Sum of Lower Semicontinuous Functions is Lower Semicontinuous Within a Set
Informal description
Let $\alpha$ be a topological space, $\gamma$ an ordered additive monoid, and $s \subseteq \alpha$. Given a finite index set $a$ and a family of functions $f_i : \alpha \to \gamma$ for $i \in a$, if each $f_i$ is lower semicontinuous at $x$ within $s$, then the finite sum $\sum_{i \in a} f_i$ is also lower semicontinuous at $x$ within $s$.
lowerSemicontinuousAt_sum theorem
{f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, LowerSemicontinuousAt (f i) x) : LowerSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x
Full source 
theorem lowerSemicontinuousAt_sum {f : ι → α → γ} {a : Finset ι}
    (ha : ∀ i ∈ a, LowerSemicontinuousAt (f i) x) :
    LowerSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x := by
  simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  exact lowerSemicontinuousWithinAt_sum ha
Finite Sum of Lower Semicontinuous Functions is Lower Semicontinuous at a Point
Informal description
Let $\alpha$ be a topological space, $\gamma$ an ordered additive monoid, and $x \in \alpha$. Given a finite index set $a$ and a family of functions $f_i : \alpha \to \gamma$ for $i \in a$, if each $f_i$ is lower semicontinuous at $x$, then the finite sum $\sum_{i \in a} f_i$ is also lower semicontinuous at $x$.
lowerSemicontinuousOn_sum theorem
{f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, LowerSemicontinuousOn (f i) s) : LowerSemicontinuousOn (fun z => ∑ i ∈ a, f i z) s
Full source 
theorem lowerSemicontinuousOn_sum {f : ι → α → γ} {a : Finset ι}
    (ha : ∀ i ∈ a, LowerSemicontinuousOn (f i) s) :
    LowerSemicontinuousOn (fun z => ∑ i ∈ a, f i z) s := fun x hx =>
  lowerSemicontinuousWithinAt_sum fun i hi => ha i hi x hx
Finite Sum of Lower Semicontinuous Functions is Lower Semicontinuous on a Set
Informal description
Let $\alpha$ be a topological space, $\gamma$ an ordered additive monoid, and $s \subseteq \alpha$. Given a finite index set $a$ and a family of functions $f_i : \alpha \to \gamma$ for $i \in a$, if each $f_i$ is lower semicontinuous on $s$, then the finite sum $\sum_{i \in a} f_i$ is also lower semicontinuous on $s$.
lowerSemicontinuous_sum theorem
{f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, LowerSemicontinuous (f i)) : LowerSemicontinuous fun z => ∑ i ∈ a, f i z
Full source 
theorem lowerSemicontinuous_sum {f : ι → α → γ} {a : Finset ι}
    (ha : ∀ i ∈ a, LowerSemicontinuous (f i)) : LowerSemicontinuous fun z => ∑ i ∈ a, f i z :=
  fun x => lowerSemicontinuousAt_sum fun i hi => ha i hi x
Finite Sum of Lower Semicontinuous Functions is Lower Semicontinuous
Informal description
Let $\alpha$ be a topological space, $\gamma$ an ordered additive monoid, and $f_i : \alpha \to \gamma$ a family of functions indexed by a finite set $a$. If each $f_i$ is lower semicontinuous, then the finite sum $\sum_{i \in a} f_i$ is also lower semicontinuous.
lowerSemicontinuousWithinAt_ciSup theorem
{f : ι → α → δ'} (bdd : ∀ᶠ y in 𝓝[s] x, BddAbove (range fun i => f i y)) (h : ∀ i, LowerSemicontinuousWithinAt (f i) s x) : LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x
Full source 
theorem lowerSemicontinuousWithinAt_ciSup {f : ι → α → δ'}
    (bdd : ∀ᶠ y in 𝓝[s] x, BddAbove (range fun i => f i y))
    (h : ∀ i, LowerSemicontinuousWithinAt (f i) s x) :
    LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x := by
  cases isEmpty_or_nonempty ι
  · simpa only [iSup_of_empty'] using lowerSemicontinuousWithinAt_const
  · intro y hy
    rcases exists_lt_of_lt_ciSup hy with ⟨i, hi⟩
    filter_upwards [h i y hi, bdd] with y hy hy' using hy.trans_le (le_ciSup hy' i)
Supremum of a Family of Lower Semicontinuous Functions is Lower Semicontinuous Under Boundedness Condition
Informal description
Let $\alpha$ and $\delta'$ be topological and conditionally complete linear order spaces respectively, and let $s \subseteq \alpha$ and $x \in \alpha$. Given a family of functions $f_i : \alpha \to \delta'$ indexed by $i \in \iota$, suppose that: 1. For all $y$ in a neighborhood of $x$ within $s$, the set $\{f_i(y) \mid i \in \iota\}$ is bounded above. 2. Each $f_i$ is lower semicontinuous at $x$ within $s$. Then the function $x' \mapsto \sup_{i} f_i(x')$ is lower semicontinuous at $x$ within $s$.
lowerSemicontinuousWithinAt_iSup theorem
{f : ι → α → δ} (h : ∀ i, LowerSemicontinuousWithinAt (f i) s x) : LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x
Full source 
theorem lowerSemicontinuousWithinAt_iSup {f : ι → α → δ}
    (h : ∀ i, LowerSemicontinuousWithinAt (f i) s x) :
    LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x :=
  lowerSemicontinuousWithinAt_ciSup (by simp) h
Supremum of Lower Semicontinuous Functions is Lower Semicontinuous Within a Set
Informal description
Let $\alpha$ be a topological space, $\delta$ a conditionally complete linear order, $s \subseteq \alpha$, and $x \in \alpha$. Given a family of functions $f_i : \alpha \to \delta$ indexed by $i \in \iota$, if each $f_i$ is lower semicontinuous at $x$ within $s$, then the function $x' \mapsto \sup_{i} f_i(x')$ is also lower semicontinuous at $x$ within $s$.
lowerSemicontinuousWithinAt_biSup theorem
{p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, LowerSemicontinuousWithinAt (f i hi) s x) : LowerSemicontinuousWithinAt (fun x' => ⨆ (i) (hi), f i hi x') s x
Full source 
theorem lowerSemicontinuousWithinAt_biSup {p : ι → Prop} {f : ∀ i, p i → α → δ}
    (h : ∀ i hi, LowerSemicontinuousWithinAt (f i hi) s x) :
    LowerSemicontinuousWithinAt (fun x' => ⨆ (i) (hi), f i hi x') s x :=
  lowerSemicontinuousWithinAt_iSup fun i => lowerSemicontinuousWithinAt_iSup fun hi => h i hi
Bounded Supremum of Lower Semicontinuous Functions is Lower Semicontinuous Within a Set
Informal description
Let $\alpha$ be a topological space, $\delta$ a conditionally complete linear order, $s \subseteq \alpha$, and $x \in \alpha$. Given a family of functions $f_i : \alpha \to \delta$ indexed by $i \in \iota$ with predicates $p_i$, if for each $i$ where $p_i$ holds, the function $f_i$ is lower semicontinuous at $x$ within $s$, then the function $x' \mapsto \sup_{i, p_i} f_i(x')$ is also lower semicontinuous at $x$ within $s$.
lowerSemicontinuousAt_ciSup theorem
{f : ι → α → δ'} (bdd : ∀ᶠ y in 𝓝 x, BddAbove (range fun i => f i y)) (h : ∀ i, LowerSemicontinuousAt (f i) x) : LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x
Full source 
theorem lowerSemicontinuousAt_ciSup {f : ι → α → δ'}
    (bdd : ∀ᶠ y in 𝓝 x, BddAbove (range fun i => f i y)) (h : ∀ i, LowerSemicontinuousAt (f i) x) :
    LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x := by
  simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  rw [← nhdsWithin_univ] at bdd
  exact lowerSemicontinuousWithinAt_ciSup bdd h
Supremum of a Bounded Family of Lower Semicontinuous Functions is Lower Semicontinuous at a Point
Informal description
Let $\alpha$ be a topological space and $\delta'$ a conditionally complete linear order. Given a family of functions $f_i : \alpha \to \delta'$ indexed by $i \in \iota$, suppose that: 1. For all $y$ in a neighborhood of $x \in \alpha$, the set $\{f_i(y) \mid i \in \iota\}$ is bounded above. 2. Each $f_i$ is lower semicontinuous at $x$. Then the function $x' \mapsto \sup_{i} f_i(x')$ is lower semicontinuous at $x$.
lowerSemicontinuousAt_iSup theorem
{f : ι → α → δ} (h : ∀ i, LowerSemicontinuousAt (f i) x) : LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x
Full source 
theorem lowerSemicontinuousAt_iSup {f : ι → α → δ} (h : ∀ i, LowerSemicontinuousAt (f i) x) :
    LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x :=
  lowerSemicontinuousAt_ciSup (by simp) h
Pointwise Supremum of Lower Semicontinuous Functions is Lower Semicontinuous at a Point
Informal description
Let $\alpha$ be a topological space and $\delta$ a conditionally complete linear order. Given a family of functions $f_i : \alpha \to \delta$ indexed by $i \in \iota$, if each $f_i$ is lower semicontinuous at a point $x \in \alpha$, then the pointwise supremum function $x' \mapsto \sup_{i} f_i(x')$ is also lower semicontinuous at $x$.
lowerSemicontinuousAt_biSup theorem
{p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, LowerSemicontinuousAt (f i hi) x) : LowerSemicontinuousAt (fun x' => ⨆ (i) (hi), f i hi x') x
Full source 
theorem lowerSemicontinuousAt_biSup {p : ι → Prop} {f : ∀ i, p i → α → δ}
    (h : ∀ i hi, LowerSemicontinuousAt (f i hi) x) :
    LowerSemicontinuousAt (fun x' => ⨆ (i) (hi), f i hi x') x :=
  lowerSemicontinuousAt_iSup fun i => lowerSemicontinuousAt_iSup fun hi => h i hi
Pointwise Supremum of a Family of Lower Semicontinuous Functions is Lower Semicontinuous at a Point
Informal description
Let $\alpha$ be a topological space and $\delta$ a complete linear order. Given a family of functions $f_i : \alpha \to \delta$ indexed by $i \in \iota$ with predicates $p_i$, if for each $i$ with $p_i$ true, the function $f_i$ is lower semicontinuous at a point $x \in \alpha$, then the pointwise supremum function $x' \mapsto \sup_{i, p_i} f_i(x')$ is also lower semicontinuous at $x$.
lowerSemicontinuousOn_ciSup theorem
{f : ι → α → δ'} (bdd : ∀ x ∈ s, BddAbove (range fun i => f i x)) (h : ∀ i, LowerSemicontinuousOn (f i) s) : LowerSemicontinuousOn (fun x' => ⨆ i, f i x') s
Full source 
theorem lowerSemicontinuousOn_ciSup {f : ι → α → δ'}
    (bdd : ∀ x ∈ s, BddAbove (range fun i => f i x)) (h : ∀ i, LowerSemicontinuousOn (f i) s) :
    LowerSemicontinuousOn (fun x' => ⨆ i, f i x') s := fun x hx =>
  lowerSemicontinuousWithinAt_ciSup (eventually_nhdsWithin_of_forall bdd) fun i => h i x hx
Pointwise Supremum of Bounded Family of Lower Semicontinuous Functions is Lower Semicontinuous on a Set
Informal description
Let $\alpha$ be a topological space and $\delta'$ a conditionally complete linear order. Given a family of functions $f_i : \alpha \to \delta'$ indexed by $i \in \iota$ and a set $s \subseteq \alpha$, suppose that: 1. For every $x \in s$, the set $\{f_i(x) \mid i \in \iota\}$ is bounded above. 2. Each function $f_i$ is lower semicontinuous on $s$. Then the pointwise supremum function $x' \mapsto \sup_{i} f_i(x')$ is lower semicontinuous on $s$.
lowerSemicontinuousOn_iSup theorem
{f : ι → α → δ} (h : ∀ i, LowerSemicontinuousOn (f i) s) : LowerSemicontinuousOn (fun x' => ⨆ i, f i x') s
Full source 
theorem lowerSemicontinuousOn_iSup {f : ι → α → δ} (h : ∀ i, LowerSemicontinuousOn (f i) s) :
    LowerSemicontinuousOn (fun x' => ⨆ i, f i x') s :=
  lowerSemicontinuousOn_ciSup (by simp) h
Pointwise Supremum of Lower Semicontinuous Functions is Lower Semicontinuous on a Set
Informal description
Let $\alpha$ be a topological space, $\delta$ a complete linear order, and $s \subseteq \alpha$ a subset. Given a family of functions $f_i : \alpha \to \delta$ indexed by $i \in \iota$, if each $f_i$ is lower semicontinuous on $s$, then the pointwise supremum function $x' \mapsto \sup_{i} f_i(x')$ is also lower semicontinuous on $s$.
lowerSemicontinuousOn_biSup theorem
{p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, LowerSemicontinuousOn (f i hi) s) : LowerSemicontinuousOn (fun x' => ⨆ (i) (hi), f i hi x') s
Full source 
theorem lowerSemicontinuousOn_biSup {p : ι → Prop} {f : ∀ i, p i → α → δ}
    (h : ∀ i hi, LowerSemicontinuousOn (f i hi) s) :
    LowerSemicontinuousOn (fun x' => ⨆ (i) (hi), f i hi x') s :=
  lowerSemicontinuousOn_iSup fun i => lowerSemicontinuousOn_iSup fun hi => h i hi
Pointwise Supremum of Conditionally Indexed Lower Semicontinuous Functions is Lower Semicontinuous on a Set
Informal description
Let $\alpha$ be a topological space, $\delta$ a complete linear order, and $s \subseteq \alpha$ a subset. Given a family of functions $f_i : \alpha \to \delta$ indexed by $i \in \iota$ with predicates $p_i$, if for each $i$ with $p_i$ the function $f_i$ is lower semicontinuous on $s$, then the pointwise supremum function $x' \mapsto \sup_{i, p_i} f_i(x')$ is also lower semicontinuous on $s$.
lowerSemicontinuous_ciSup theorem
{f : ι → α → δ'} (bdd : ∀ x, BddAbove (range fun i => f i x)) (h : ∀ i, LowerSemicontinuous (f i)) : LowerSemicontinuous fun x' => ⨆ i, f i x'
Full source 
theorem lowerSemicontinuous_ciSup {f : ι → α → δ'} (bdd : ∀ x, BddAbove (range fun i => f i x))
    (h : ∀ i, LowerSemicontinuous (f i)) : LowerSemicontinuous fun x' => ⨆ i, f i x' := fun x =>
  lowerSemicontinuousAt_ciSup (Eventually.of_forall bdd) fun i => h i x
Supremum of a Bounded Family of Lower Semicontinuous Functions is Lower Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\delta'$ a conditionally complete linear order. Given a family of functions $f_i : \alpha \to \delta'$ indexed by $i \in \iota$, suppose that: 1. For every $x \in \alpha$, the set $\{f_i(x) \mid i \in \iota\}$ is bounded above. 2. Each $f_i$ is lower semicontinuous. Then the function $x' \mapsto \sup_{i} f_i(x')$ is lower semicontinuous.
lowerSemicontinuous_iSup theorem
{f : ι → α → δ} (h : ∀ i, LowerSemicontinuous (f i)) : LowerSemicontinuous fun x' => ⨆ i, f i x'
Full source 
theorem lowerSemicontinuous_iSup {f : ι → α → δ} (h : ∀ i, LowerSemicontinuous (f i)) :
    LowerSemicontinuous fun x' => ⨆ i, f i x' :=
  lowerSemicontinuous_ciSup (by simp) h
Supremum of Lower Semicontinuous Functions is Lower Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\delta$ a complete linear order. Given a family of lower semicontinuous functions $f_i : \alpha \to \delta$ indexed by $i \in \iota$, the pointwise supremum function $x' \mapsto \sup_{i} f_i(x')$ is lower semicontinuous.
lowerSemicontinuous_biSup theorem
{p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, LowerSemicontinuous (f i hi)) : LowerSemicontinuous fun x' => ⨆ (i) (hi), f i hi x'
Full source 
theorem lowerSemicontinuous_biSup {p : ι → Prop} {f : ∀ i, p i → α → δ}
    (h : ∀ i hi, LowerSemicontinuous (f i hi)) :
    LowerSemicontinuous fun x' => ⨆ (i) (hi), f i hi x' :=
  lowerSemicontinuous_iSup fun i => lowerSemicontinuous_iSup fun hi => h i hi
Supremum of a Family of Lower Semicontinuous Functions is Lower Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\delta$ a complete linear order. Given a family of functions $f_i : \alpha \to \delta$ indexed by $i \in \iota$ with predicates $p : \iota \to \text{Prop}$, if for each $i$ with $p(i)$ the function $f_i$ is lower semicontinuous, then the pointwise supremum function $x' \mapsto \sup_{i, p(i)} f_i(x')$ is lower semicontinuous.
lowerSemicontinuousWithinAt_tsum theorem
{f : ι → α → ℝ≥0∞} (h : ∀ i, LowerSemicontinuousWithinAt (f i) s x) : LowerSemicontinuousWithinAt (fun x' => ∑' i, f i x') s x
Full source 
theorem lowerSemicontinuousWithinAt_tsum {f : ι → α → ℝ≥0∞}
    (h : ∀ i, LowerSemicontinuousWithinAt (f i) s x) :
    LowerSemicontinuousWithinAt (fun x' => ∑' i, f i x') s x := by
  simp_rw [ENNReal.tsum_eq_iSup_sum]
  refine lowerSemicontinuousWithinAt_iSup fun b => ?_
  exact lowerSemicontinuousWithinAt_sum fun i _hi => h i
Infinite Sum of Lower Semicontinuous Functions is Lower Semicontinuous Within a Set
Informal description
Let $\alpha$ be a topological space, $s \subseteq \alpha$, and $x \in \alpha$. Given a family of functions $f_i : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ indexed by $i \in \iota$, if each $f_i$ is lower semicontinuous at $x$ within $s$, then the function $x' \mapsto \sum_{i} f_i(x')$ is also lower semicontinuous at $x$ within $s$.
lowerSemicontinuousAt_tsum theorem
{f : ι → α → ℝ≥0∞} (h : ∀ i, LowerSemicontinuousAt (f i) x) : LowerSemicontinuousAt (fun x' => ∑' i, f i x') x
Full source 
theorem lowerSemicontinuousAt_tsum {f : ι → α → ℝ≥0∞} (h : ∀ i, LowerSemicontinuousAt (f i) x) :
    LowerSemicontinuousAt (fun x' => ∑' i, f i x') x := by
  simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  exact lowerSemicontinuousWithinAt_tsum h
Infinite Sum of Lower Semicontinuous Functions is Lower Semicontinuous at a Point
Informal description
Let $\alpha$ be a topological space and $x \in \alpha$. Given a family of functions $f_i : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ indexed by $i \in \iota$, if each $f_i$ is lower semicontinuous at $x$, then the function $x' \mapsto \sum_{i} f_i(x')$ is also lower semicontinuous at $x$.
lowerSemicontinuousOn_tsum theorem
{f : ι → α → ℝ≥0∞} (h : ∀ i, LowerSemicontinuousOn (f i) s) : LowerSemicontinuousOn (fun x' => ∑' i, f i x') s
Full source 
theorem lowerSemicontinuousOn_tsum {f : ι → α → ℝ≥0∞} (h : ∀ i, LowerSemicontinuousOn (f i) s) :
    LowerSemicontinuousOn (fun x' => ∑' i, f i x') s := fun x hx =>
  lowerSemicontinuousWithinAt_tsum fun i => h i x hx
Infinite Sum of Lower Semicontinuous Functions is Lower Semicontinuous on a Set
Informal description
Let $\alpha$ be a topological space and $s \subseteq \alpha$. Given a family of functions $f_i : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ indexed by $i \in \iota$, if each $f_i$ is lower semicontinuous on $s$, then the function $x' \mapsto \sum_{i} f_i(x')$ is also lower semicontinuous on $s$.
lowerSemicontinuous_tsum theorem
{f : ι → α → ℝ≥0∞} (h : ∀ i, LowerSemicontinuous (f i)) : LowerSemicontinuous fun x' => ∑' i, f i x'
Full source 
theorem lowerSemicontinuous_tsum {f : ι → α → ℝ≥0∞} (h : ∀ i, LowerSemicontinuous (f i)) :
    LowerSemicontinuous fun x' => ∑' i, f i x' := fun x => lowerSemicontinuousAt_tsum fun i => h i x
Infinite Sum of Lower Semicontinuous Functions is Lower Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\{f_i : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}\}_{i \in \iota}$ be a family of lower semicontinuous functions. Then the function $x \mapsto \sum_{i \in \iota} f_i(x)$ is lower semicontinuous.
UpperSemicontinuousWithinAt.mono theorem
(h : UpperSemicontinuousWithinAt f s x) (hst : t ⊆ s) : UpperSemicontinuousWithinAt f t x
Full source 
theorem UpperSemicontinuousWithinAt.mono (h : UpperSemicontinuousWithinAt f s x) (hst : t ⊆ s) :
    UpperSemicontinuousWithinAt f t x := fun y hy =>
  Filter.Eventually.filter_mono (nhdsWithin_mono _ hst) (h y hy)
Restriction Preserves Upper Semicontinuity Within a Set
Informal description
Let $f : \alpha \to \beta$ be a function between a topological space $\alpha$ and an ordered space $\beta$. If $f$ is upper semicontinuous at a point $x \in \alpha$ within a set $s \subseteq \alpha$, then for any subset $t \subseteq s$, $f$ is also upper semicontinuous at $x$ within $t$.
upperSemicontinuousWithinAt_univ_iff theorem
: UpperSemicontinuousWithinAt f univ x ↔ UpperSemicontinuousAt f x
Full source 
theorem upperSemicontinuousWithinAt_univ_iff :
    UpperSemicontinuousWithinAtUpperSemicontinuousWithinAt f univ x ↔ UpperSemicontinuousAt f x := by
  simp [UpperSemicontinuousWithinAt, UpperSemicontinuousAt, nhdsWithin_univ]
Equivalence of Upper Semicontinuity within Universal Set and Pointwise Upper Semicontinuity
Informal description
A function $f \colon \alpha \to \beta$ is upper semicontinuous at a point $x \in \alpha$ within the universal set $\text{univ}$ if and only if it is upper semicontinuous at $x$.
UpperSemicontinuousAt.upperSemicontinuousWithinAt theorem
(s : Set α) (h : UpperSemicontinuousAt f x) : UpperSemicontinuousWithinAt f s x
Full source 
theorem UpperSemicontinuousAt.upperSemicontinuousWithinAt (s : Set α)
    (h : UpperSemicontinuousAt f x) : UpperSemicontinuousWithinAt f s x := fun y hy =>
  Filter.Eventually.filter_mono nhdsWithin_le_nhds (h y hy)
Upper semicontinuity at a point implies upper semicontinuity within any subset at that point
Informal description
Let $f \colon \alpha \to \beta$ be a function between a topological space $\alpha$ and a preordered space $\beta$. If $f$ is upper semicontinuous at a point $x \in \alpha$, then for any subset $s \subseteq \alpha$, $f$ is upper semicontinuous at $x$ within $s$.
UpperSemicontinuousOn.upperSemicontinuousWithinAt theorem
(h : UpperSemicontinuousOn f s) (hx : x ∈ s) : UpperSemicontinuousWithinAt f s x
Full source 
theorem UpperSemicontinuousOn.upperSemicontinuousWithinAt (h : UpperSemicontinuousOn f s)
    (hx : x ∈ s) : UpperSemicontinuousWithinAt f s x :=
  h x hx
Upper Semicontinuity on a Set Implies Pointwise Upper Semicontinuity Within the Set
Informal description
If a function $f \colon \alpha \to \beta$ is upper semicontinuous on a set $s \subseteq \alpha$, then for any point $x \in s$, the function $f$ is upper semicontinuous at $x$ within $s$.
UpperSemicontinuousOn.mono theorem
(h : UpperSemicontinuousOn f s) (hst : t ⊆ s) : UpperSemicontinuousOn f t
Full source 
theorem UpperSemicontinuousOn.mono (h : UpperSemicontinuousOn f s) (hst : t ⊆ s) :
    UpperSemicontinuousOn f t := fun x hx => (h x (hst hx)).mono hst
Restriction Preserves Upper Semicontinuity on Subsets
Informal description
Let $f \colon \alpha \to \beta$ be a function from a topological space $\alpha$ to an ordered space $\beta$. If $f$ is upper semicontinuous on a set $s \subseteq \alpha$, then for any subset $t \subseteq s$, $f$ is also upper semicontinuous on $t$.
upperSemicontinuousOn_univ_iff theorem
: UpperSemicontinuousOn f univ ↔ UpperSemicontinuous f
Full source 
theorem upperSemicontinuousOn_univ_iff : UpperSemicontinuousOnUpperSemicontinuousOn f univ ↔ UpperSemicontinuous f := by
  simp [UpperSemicontinuousOn, UpperSemicontinuous, upperSemicontinuousWithinAt_univ_iff]
Upper Semicontinuity on Universal Set Equivalence
Informal description
A function $f \colon \alpha \to \beta$ is upper semicontinuous on the universal set $\text{univ} \subseteq \alpha$ if and only if it is upper semicontinuous.
UpperSemicontinuous.upperSemicontinuousAt theorem
(h : UpperSemicontinuous f) (x : α) : UpperSemicontinuousAt f x
Full source 
theorem UpperSemicontinuous.upperSemicontinuousAt (h : UpperSemicontinuous f) (x : α) :
    UpperSemicontinuousAt f x :=
  h x
Global Upper Semicontinuity Implies Pointwise Upper Semicontinuity
Informal description
If a function $f \colon \alpha \to \beta$ is upper semicontinuous, then it is upper semicontinuous at every point $x \in \alpha$.
UpperSemicontinuous.upperSemicontinuousWithinAt theorem
(h : UpperSemicontinuous f) (s : Set α) (x : α) : UpperSemicontinuousWithinAt f s x
Full source 
theorem UpperSemicontinuous.upperSemicontinuousWithinAt (h : UpperSemicontinuous f) (s : Set α)
    (x : α) : UpperSemicontinuousWithinAt f s x :=
  (h x).upperSemicontinuousWithinAt s
Global Upper Semicontinuity Implies Local Upper Semicontinuity Within Any Subset
Informal description
Let $f \colon \alpha \to \beta$ be an upper semicontinuous function between a topological space $\alpha$ and a preordered space $\beta$. Then for any subset $s \subseteq \alpha$ and any point $x \in \alpha$, the function $f$ is upper semicontinuous at $x$ within $s$.
UpperSemicontinuous.upperSemicontinuousOn theorem
(h : UpperSemicontinuous f) (s : Set α) : UpperSemicontinuousOn f s
Full source 
theorem UpperSemicontinuous.upperSemicontinuousOn (h : UpperSemicontinuous f) (s : Set α) :
    UpperSemicontinuousOn f s := fun x _hx => h.upperSemicontinuousWithinAt s x
Global Upper Semicontinuity Implies Upper Semicontinuity on Any Subset
Informal description
If a function $f \colon \alpha \to \beta$ is upper semicontinuous, then for any subset $s \subseteq \alpha$, the restriction of $f$ to $s$ is upper semicontinuous on $s$.
upperSemicontinuousWithinAt_const theorem
: UpperSemicontinuousWithinAt (fun _x => z) s x
Full source 
theorem upperSemicontinuousWithinAt_const : UpperSemicontinuousWithinAt (fun _x => z) s x :=
  fun _y hy => Filter.Eventually.of_forall fun _x => hy
Constant Functions are Upper Semicontinuous Within a Set at a Point
Informal description
For any constant function $f \colon \alpha \to \beta$ defined by $f(x) = z$ for all $x \in \alpha$, and for any subset $s \subseteq \alpha$ and point $x \in \alpha$, the function $f$ is upper semicontinuous at $x$ within $s$.
upperSemicontinuousAt_const theorem
: UpperSemicontinuousAt (fun _x => z) x
Full source 
theorem upperSemicontinuousAt_const : UpperSemicontinuousAt (fun _x => z) x := fun _y hy =>
  Filter.Eventually.of_forall fun _x => hy
Constant functions are upper semicontinuous
Informal description
The constant function $f \colon \alpha \to \beta$ defined by $f(x) = z$ for all $x \in \alpha$ is upper semicontinuous at every point $x \in \alpha$.
upperSemicontinuousOn_const theorem
: UpperSemicontinuousOn (fun _x => z) s
Full source 
theorem upperSemicontinuousOn_const : UpperSemicontinuousOn (fun _x => z) s := fun _x _hx =>
  upperSemicontinuousWithinAt_const
Constant Functions are Upper Semicontinuous on a Set
Informal description
For any constant function $f \colon \alpha \to \beta$ defined by $f(x) = z$ for all $x \in \alpha$, and for any subset $s \subseteq \alpha$, the function $f$ is upper semicontinuous on $s$.
upperSemicontinuous_const theorem
: UpperSemicontinuous fun _x : α => z
Full source 
theorem upperSemicontinuous_const : UpperSemicontinuous fun _x : α => z := fun _x =>
  upperSemicontinuousAt_const
Constant Functions are Upper Semicontinuous
Informal description
The constant function $f \colon \alpha \to \beta$ defined by $f(x) = z$ for all $x \in \alpha$ is upper semicontinuous.
IsOpen.upperSemicontinuous_indicator theorem
(hs : IsOpen s) (hy : y ≤ 0) : UpperSemicontinuous (indicator s fun _x => y)
Full source 
theorem IsOpen.upperSemicontinuous_indicator (hs : IsOpen s) (hy : y ≤ 0) :
    UpperSemicontinuous (indicator s fun _x => y) :=
  @IsOpen.lowerSemicontinuous_indicator α _ βᵒᵈ _ s y _ hs hy
Upper semicontinuity of indicator function on open set with non-positive value
Informal description
Let $s$ be an open set in a topological space $\alpha$ and let $y$ be a non-positive element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is upper semicontinuous on $\alpha$.
IsOpen.upperSemicontinuousOn_indicator theorem
(hs : IsOpen s) (hy : y ≤ 0) : UpperSemicontinuousOn (indicator s fun _x => y) t
Full source 
theorem IsOpen.upperSemicontinuousOn_indicator (hs : IsOpen s) (hy : y ≤ 0) :
    UpperSemicontinuousOn (indicator s fun _x => y) t :=
  (hs.upperSemicontinuous_indicator hy).upperSemicontinuousOn t
Upper Semicontinuity of Indicator Function on Open Set with Non-Positive Value Restricted to Any Subset
Informal description
Let $s$ be an open subset of a topological space $\alpha$, $y \leq 0$ an element in an ordered space $\beta$, and $t \subseteq \alpha$ any subset. The indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is upper semicontinuous on $t$.
IsOpen.upperSemicontinuousAt_indicator theorem
(hs : IsOpen s) (hy : y ≤ 0) : UpperSemicontinuousAt (indicator s fun _x => y) x
Full source 
theorem IsOpen.upperSemicontinuousAt_indicator (hs : IsOpen s) (hy : y ≤ 0) :
    UpperSemicontinuousAt (indicator s fun _x => y) x :=
  (hs.upperSemicontinuous_indicator hy).upperSemicontinuousAt x
Upper Semicontinuity at a Point for Indicator Function on Open Set with Non-Positive Value
Informal description
Let $s$ be an open subset of a topological space $\alpha$ and let $y \leq 0$ be an element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is upper semicontinuous at every point $x \in \alpha$.
IsOpen.upperSemicontinuousWithinAt_indicator theorem
(hs : IsOpen s) (hy : y ≤ 0) : UpperSemicontinuousWithinAt (indicator s fun _x => y) t x
Full source 
theorem IsOpen.upperSemicontinuousWithinAt_indicator (hs : IsOpen s) (hy : y ≤ 0) :
    UpperSemicontinuousWithinAt (indicator s fun _x => y) t x :=
  (hs.upperSemicontinuous_indicator hy).upperSemicontinuousWithinAt t x
Upper Semicontinuity Within Subset for Indicator Function on Open Set with Non-Positive Value
Informal description
Let $s$ be an open subset of a topological space $\alpha$, $y \leq 0$ an element in an ordered space $\beta$, and $t \subseteq \alpha$ any subset. Then the indicator function $\mathbf{1}_s(\cdot) y$ (which equals $y$ on $s$ and $0$ elsewhere) is upper semicontinuous at any point $x \in \alpha$ when restricted to $t$.
IsClosed.upperSemicontinuous_indicator theorem
(hs : IsClosed s) (hy : 0 ≤ y) : UpperSemicontinuous (indicator s fun _x => y)
Full source 
theorem IsClosed.upperSemicontinuous_indicator (hs : IsClosed s) (hy : 0 ≤ y) :
    UpperSemicontinuous (indicator s fun _x => y) :=
  @IsClosed.lowerSemicontinuous_indicator α _ βᵒᵈ _ s y _ hs hy
Upper Semicontinuity of Indicator Function on Closed Set with Non-Negative Value
Informal description
Let $s$ be a closed subset of a topological space $\alpha$ and let $y$ be a non-negative element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is upper semicontinuous on $\alpha$.
IsClosed.upperSemicontinuousOn_indicator theorem
(hs : IsClosed s) (hy : 0 ≤ y) : UpperSemicontinuousOn (indicator s fun _x => y) t
Full source 
theorem IsClosed.upperSemicontinuousOn_indicator (hs : IsClosed s) (hy : 0 ≤ y) :
    UpperSemicontinuousOn (indicator s fun _x => y) t :=
  (hs.upperSemicontinuous_indicator hy).upperSemicontinuousOn t
Upper Semicontinuity of Indicator Function on Closed Set with Non-Negative Value Restricted to Any Subset
Informal description
Let $s$ be a closed subset of a topological space $\alpha$ and let $y$ be a non-negative element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is upper semicontinuous on any subset $t \subseteq \alpha$.
IsClosed.upperSemicontinuousAt_indicator theorem
(hs : IsClosed s) (hy : 0 ≤ y) : UpperSemicontinuousAt (indicator s fun _x => y) x
Full source 
theorem IsClosed.upperSemicontinuousAt_indicator (hs : IsClosed s) (hy : 0 ≤ y) :
    UpperSemicontinuousAt (indicator s fun _x => y) x :=
  (hs.upperSemicontinuous_indicator hy).upperSemicontinuousAt x
Upper Semicontinuity at a Point of Indicator Function on Closed Set with Non-Negative Value
Informal description
Let $s$ be a closed subset of a topological space $\alpha$ and let $y$ be a non-negative element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is upper semicontinuous at every point $x \in \alpha$.
IsClosed.upperSemicontinuousWithinAt_indicator theorem
(hs : IsClosed s) (hy : 0 ≤ y) : UpperSemicontinuousWithinAt (indicator s fun _x => y) t x
Full source 
theorem IsClosed.upperSemicontinuousWithinAt_indicator (hs : IsClosed s) (hy : 0 ≤ y) :
    UpperSemicontinuousWithinAt (indicator s fun _x => y) t x :=
  (hs.upperSemicontinuous_indicator hy).upperSemicontinuousWithinAt t x
Upper Semicontinuity Within a Subset for Indicator Function on Closed Set with Non-Negative Value
Informal description
Let $s$ be a closed subset of a topological space $\alpha$ and let $y$ be a non-negative element in an ordered space $\beta$. Then the indicator function $\mathbf{1}_s(\cdot) y$ (defined as $y$ on $s$ and $0$ elsewhere) is upper semicontinuous at a point $x \in \alpha$ within any subset $t \subseteq \alpha$.
upperSemicontinuous_iff_isOpen_preimage theorem
: UpperSemicontinuous f ↔ ∀ y, IsOpen (f ⁻¹' Iio y)
Full source 
theorem upperSemicontinuous_iff_isOpen_preimage :
    UpperSemicontinuousUpperSemicontinuous f ↔ ∀ y, IsOpen (f ⁻¹' Iio y) :=
  ⟨fun H y => isOpen_iff_mem_nhds.2 fun x hx => H x y hx, fun H _x y y_lt =>
    IsOpen.mem_nhds (H y) y_lt⟩
Characterization of Upper Semicontinuity via Open Preimages of Left-Infinite Intervals
Informal description
A function $f \colon \alpha \to \beta$ from a topological space $\alpha$ to a linearly ordered space $\beta$ is upper semicontinuous if and only if for every $y \in \beta$, the preimage $f^{-1}((-\infty, y))$ is an open set in $\alpha$.
UpperSemicontinuous.isOpen_preimage theorem
(hf : UpperSemicontinuous f) (y : β) : IsOpen (f ⁻¹' Iio y)
Full source 
theorem UpperSemicontinuous.isOpen_preimage (hf : UpperSemicontinuous f) (y : β) :
    IsOpen (f ⁻¹' Iio y) :=
  upperSemicontinuous_iff_isOpen_preimage.1 hf y
Open Preimage Characterization of Upper Semicontinuous Functions
Informal description
Let $f \colon \alpha \to \beta$ be an upper semicontinuous function from a topological space $\alpha$ to a linearly ordered space $\beta$. Then for any $y \in \beta$, the preimage $f^{-1}((-\infty, y))$ is an open subset of $\alpha$.
upperSemicontinuous_iff_isClosed_preimage theorem
{f : α → γ} : UpperSemicontinuous f ↔ ∀ y, IsClosed (f ⁻¹' Ici y)
Full source 
theorem upperSemicontinuous_iff_isClosed_preimage {f : α → γ} :
    UpperSemicontinuousUpperSemicontinuous f ↔ ∀ y, IsClosed (f ⁻¹' Ici y) := by
  rw [upperSemicontinuous_iff_isOpen_preimage]
  simp only [← isOpen_compl_iff, ← preimage_compl, compl_Ici]
Characterization of upper semicontinuity via closed preimages of right-closed intervals
Informal description
A function $f \colon \alpha \to \gamma$ from a topological space $\alpha$ to a linearly ordered space $\gamma$ is upper semicontinuous if and only if for every $y \in \gamma$, the preimage $f^{-1}([y, \infty))$ is a closed set in $\alpha$.
UpperSemicontinuous.isClosed_preimage theorem
{f : α → γ} (hf : UpperSemicontinuous f) (y : γ) : IsClosed (f ⁻¹' Ici y)
Full source 
theorem UpperSemicontinuous.isClosed_preimage {f : α → γ} (hf : UpperSemicontinuous f) (y : γ) :
    IsClosed (f ⁻¹' Ici y) :=
  upperSemicontinuous_iff_isClosed_preimage.1 hf y
Closed Preimage Property of Upper Semicontinuous Functions
Informal description
Let $f \colon \alpha \to \gamma$ be an upper semicontinuous function from a topological space $\alpha$ to a linearly ordered space $\gamma$. Then for any $y \in \gamma$, the preimage $f^{-1}([y, \infty))$ is a closed subset of $\alpha$.
ContinuousWithinAt.upperSemicontinuousWithinAt theorem
{f : α → γ} (h : ContinuousWithinAt f s x) : UpperSemicontinuousWithinAt f s x
Full source 
theorem ContinuousWithinAt.upperSemicontinuousWithinAt {f : α → γ} (h : ContinuousWithinAt f s x) :
    UpperSemicontinuousWithinAt f s x := fun _y hy => h (Iio_mem_nhds hy)
Continuous functions are upper semicontinuous within a set
Informal description
Let $f \colon \alpha \to \gamma$ be a function between topological spaces, with $\gamma$ linearly ordered. If $f$ is continuous at $x \in \alpha$ within a set $s \subseteq \alpha$, then $f$ is upper semicontinuous at $x$ within $s$. More precisely, for any $y > f(x)$, there exists a neighborhood $U$ of $x$ in $s$ such that for all $x' \in U$, we have $f(x') < y$.
ContinuousAt.upperSemicontinuousAt theorem
{f : α → γ} (h : ContinuousAt f x) : UpperSemicontinuousAt f x
Full source 
theorem ContinuousAt.upperSemicontinuousAt {f : α → γ} (h : ContinuousAt f x) :
    UpperSemicontinuousAt f x := fun _y hy => h (Iio_mem_nhds hy)
Continuous functions are upper semicontinuous at points of continuity
Informal description
Let $f \colon \alpha \to \gamma$ be a function between topological spaces. If $f$ is continuous at a point $x \in \alpha$, then $f$ is upper semicontinuous at $x$. That is, for any $y > f(x)$, there exists a neighborhood $U$ of $x$ such that for all $x' \in U$, $f(x') < y$.
ContinuousOn.upperSemicontinuousOn theorem
{f : α → γ} (h : ContinuousOn f s) : UpperSemicontinuousOn f s
Full source 
theorem ContinuousOn.upperSemicontinuousOn {f : α → γ} (h : ContinuousOn f s) :
    UpperSemicontinuousOn f s := fun x hx => (h x hx).upperSemicontinuousWithinAt
Continuous Functions are Upper Semicontinuous on a Set
Informal description
Let $f \colon \alpha \to \gamma$ be a function between topological spaces, where $\gamma$ is a linearly ordered set. If $f$ is continuous on a set $s \subseteq \alpha$, then $f$ is upper semicontinuous on $s$. That is, for every $x \in s$ and any $y > f(x)$, there exists a neighborhood $U$ of $x$ in $s$ such that $f(x') < y$ for all $x' \in U$.
Continuous.upperSemicontinuous theorem
{f : α → γ} (h : Continuous f) : UpperSemicontinuous f
Full source 
theorem Continuous.upperSemicontinuous {f : α → γ} (h : Continuous f) : UpperSemicontinuous f :=
  fun _x => h.continuousAt.upperSemicontinuousAt
Continuous Functions are Upper Semicontinuous
Informal description
Let $f \colon \alpha \to \gamma$ be a continuous function between topological spaces. Then $f$ is upper semicontinuous, meaning that for every $x \in \alpha$ and any $y > f(x)$, there exists a neighborhood $U$ of $x$ such that $f(x') < y$ for all $x' \in U$.
upperSemicontinuousWithinAt_iff_limsup_le theorem
{f : α → γ} : UpperSemicontinuousWithinAt f s x ↔ limsup f (𝓝[s] x) ≤ f x
Full source 
theorem upperSemicontinuousWithinAt_iff_limsup_le {f : α → γ} :
    UpperSemicontinuousWithinAtUpperSemicontinuousWithinAt f s x ↔ limsup f (𝓝[s] x) ≤ f x :=
  lowerSemicontinuousWithinAt_iff_le_liminf (γ := γᵒᵈ)
Characterization of Upper Semicontinuity via Limit Superior: $f$ is upper semicontinuous at $x$ within $s$ if and only if $\limsup_{x' \to x, x' \in s} f(x') \leq f(x)$
Informal description
Let $f : \alpha \to \gamma$ be a function from a topological space $\alpha$ to a conditionally complete linear order $\gamma$. Then $f$ is upper semicontinuous at a point $x \in \alpha$ within a set $s \subseteq \alpha$ if and only if $\limsup_{x' \to x, x' \in s} f(x') \leq f(x)$, where the limit superior is taken with respect to the neighborhood filter of $x$ restricted to $s$.
upperSemicontinuousAt_iff_limsup_le theorem
{f : α → γ} : UpperSemicontinuousAt f x ↔ limsup f (𝓝 x) ≤ f x
Full source 
theorem upperSemicontinuousAt_iff_limsup_le {f : α → γ} :
    UpperSemicontinuousAtUpperSemicontinuousAt f x ↔ limsup f (𝓝 x) ≤ f x :=
  lowerSemicontinuousAt_iff_le_liminf (γ := γᵒᵈ)
Characterization of Upper Semicontinuity at a Point via Limit Superior: $\limsup_{x' \to x} f(x') \leq f(x)$
Informal description
Let $f \colon \alpha \to \gamma$ be a function from a topological space $\alpha$ to a conditionally complete linear order $\gamma$. Then $f$ is upper semicontinuous at a point $x \in \alpha$ if and only if the limit superior of $f$ as $x'$ approaches $x$ satisfies $\limsup_{x' \to x} f(x') \leq f(x)$.
upperSemicontinuous_iff_limsup_le theorem
{f : α → γ} : UpperSemicontinuous f ↔ ∀ x, limsup f (𝓝 x) ≤ f x
Full source 
theorem upperSemicontinuous_iff_limsup_le {f : α → γ} :
    UpperSemicontinuousUpperSemicontinuous f ↔ ∀ x, limsup f (𝓝 x) ≤ f x :=
  lowerSemicontinuous_iff_le_liminf (γ := γᵒᵈ)
Characterization of Upper Semicontinuity via Limit Superior
Informal description
A function $f \colon \alpha \to \gamma$ from a topological space $\alpha$ to a conditionally complete linear order $\gamma$ is upper semicontinuous if and only if for every point $x \in \alpha$, the limit superior of $f$ as the argument approaches $x$ is less than or equal to $f(x)$. In other words, $f$ is upper semicontinuous precisely when at every point $x$, the largest limit point of $f$ near $x$ does not exceed the function value $f(x)$.
upperSemicontinuousOn_iff_limsup_le theorem
{f : α → γ} : UpperSemicontinuousOn f s ↔ ∀ x ∈ s, limsup f (𝓝[s] x) ≤ f x
Full source 
theorem upperSemicontinuousOn_iff_limsup_le {f : α → γ} :
    UpperSemicontinuousOnUpperSemicontinuousOn f s ↔ ∀ x ∈ s, limsup f (𝓝[s] x) ≤ f x :=
  lowerSemicontinuousOn_iff_le_liminf (γ := γᵒᵈ)
Characterization of Upper Semicontinuity via Limit Superior on a Set
Informal description
A function $f : \alpha \to \gamma$ is upper semicontinuous on a set $s \subseteq \alpha$ if and only if for every point $x \in s$, the limit superior of $f$ as $x'$ approaches $x$ within $s$ is less than or equal to $f(x)$.
upperSemicontinuous_iff_IsClosed_hypograph theorem
{f : α → γ} : UpperSemicontinuous f ↔ IsClosed {p : α × γ | p.2 ≤ f p.1}
Full source 
theorem upperSemicontinuous_iff_IsClosed_hypograph {f : α → γ} :
    UpperSemicontinuousUpperSemicontinuous f ↔ IsClosed {p : α × γ | p.2 ≤ f p.1} :=
  lowerSemicontinuous_iff_isClosed_epigraph (γ := γᵒᵈ)
Characterization of Upper Semicontinuity via Closed Hypograph
Informal description
A function $f \colon \alpha \to \gamma$ from a topological space $\alpha$ to a preordered space $\gamma$ is upper semicontinuous if and only if its hypograph $\{(x,y) \in \alpha \times \gamma \mid y \leq f(x)\}$ is a closed subset of $\alpha \times \gamma$.
ContinuousAt.comp_upperSemicontinuousWithinAt theorem
{g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousWithinAt f s x) (gmon : Monotone g) : UpperSemicontinuousWithinAt (g ∘ f) s x
Full source 
theorem ContinuousAt.comp_upperSemicontinuousWithinAt {g : γ → δ} {f : α → γ}
    (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousWithinAt f s x) (gmon : Monotone g) :
    UpperSemicontinuousWithinAt (g ∘ f) s x :=
  @ContinuousAt.comp_lowerSemicontinuousWithinAt α _ x s γᵒᵈ _ _ _ δᵒᵈ _ _ _ g f hg hf gmon.dual
Monotone Continuous Composition Preserves Upper Semicontinuity Within a Set
Informal description
Let $f \colon \alpha \to \gamma$ be a function that is upper semicontinuous at a point $x$ within a set $s \subseteq \alpha$, and let $g \colon \gamma \to \delta$ be a continuous function at $f(x)$. If $g$ is monotone, then the composition $g \circ f$ is upper semicontinuous at $x$ within $s$.
ContinuousAt.comp_upperSemicontinuousAt theorem
{g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousAt f x) (gmon : Monotone g) : UpperSemicontinuousAt (g ∘ f) x
Full source 
theorem ContinuousAt.comp_upperSemicontinuousAt {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x))
    (hf : UpperSemicontinuousAt f x) (gmon : Monotone g) : UpperSemicontinuousAt (g ∘ f) x :=
  @ContinuousAt.comp_lowerSemicontinuousAt α _ x γᵒᵈ _ _ _ δᵒᵈ _ _ _ g f hg hf gmon.dual
Monotone Continuous Composition Preserves Upper Semicontinuity at a Point
Informal description
Let $f \colon \alpha \to \gamma$ be a function that is upper semicontinuous at a point $x \in \alpha$, and let $g \colon \gamma \to \delta$ be a continuous function at $f(x)$. If $g$ is monotone, then the composition $g \circ f$ is upper semicontinuous at $x$.
Continuous.comp_upperSemicontinuousOn theorem
{g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : UpperSemicontinuousOn f s) (gmon : Monotone g) : UpperSemicontinuousOn (g ∘ f) s
Full source 
theorem Continuous.comp_upperSemicontinuousOn {g : γ → δ} {f : α → γ} (hg : Continuous g)
    (hf : UpperSemicontinuousOn f s) (gmon : Monotone g) : UpperSemicontinuousOn (g ∘ f) s :=
  fun x hx => hg.continuousAt.comp_upperSemicontinuousWithinAt (hf x hx) gmon
Monotone Continuous Composition Preserves Upper Semicontinuity on a Set
Informal description
Let $f \colon \alpha \to \gamma$ be an upper semicontinuous function on a set $s \subseteq \alpha$, and let $g \colon \gamma \to \delta$ be a continuous function. If $g$ is monotone, then the composition $g \circ f$ is upper semicontinuous on $s$.
Continuous.comp_upperSemicontinuous theorem
{g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : UpperSemicontinuous f) (gmon : Monotone g) : UpperSemicontinuous (g ∘ f)
Full source 
theorem Continuous.comp_upperSemicontinuous {g : γ → δ} {f : α → γ} (hg : Continuous g)
    (hf : UpperSemicontinuous f) (gmon : Monotone g) : UpperSemicontinuous (g ∘ f) := fun x =>
  hg.continuousAt.comp_upperSemicontinuousAt (hf x) gmon
Monotone Continuous Composition Preserves Upper Semicontinuity
Informal description
Let $f \colon \alpha \to \gamma$ be an upper semicontinuous function and $g \colon \gamma \to \delta$ be a continuous function. If $g$ is monotone, then the composition $g \circ f$ is upper semicontinuous.
ContinuousAt.comp_upperSemicontinuousWithinAt_antitone theorem
{g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousWithinAt f s x) (gmon : Antitone g) : LowerSemicontinuousWithinAt (g ∘ f) s x
Full source 
theorem ContinuousAt.comp_upperSemicontinuousWithinAt_antitone {g : γ → δ} {f : α → γ}
    (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousWithinAt f s x) (gmon : Antitone g) :
    LowerSemicontinuousWithinAt (g ∘ f) s x :=
  @ContinuousAt.comp_upperSemicontinuousWithinAt α _ x s γ _ _ _ δᵒᵈ _ _ _ g f hg hf gmon
Antitone Continuous Composition Transforms Upper Semicontinuity to Lower Semicontinuity Within a Set
Informal description
Let $f \colon \alpha \to \gamma$ be a function that is upper semicontinuous at a point $x$ within a set $s \subseteq \alpha$, and let $g \colon \gamma \to \delta$ be a function that is continuous at $f(x)$. If $g$ is antitone (order-reversing), then the composition $g \circ f$ is lower semicontinuous at $x$ within $s$.
ContinuousAt.comp_upperSemicontinuousAt_antitone theorem
{g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousAt f x) (gmon : Antitone g) : LowerSemicontinuousAt (g ∘ f) x
Full source 
theorem ContinuousAt.comp_upperSemicontinuousAt_antitone {g : γ → δ} {f : α → γ}
    (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousAt f x) (gmon : Antitone g) :
    LowerSemicontinuousAt (g ∘ f) x :=
  @ContinuousAt.comp_upperSemicontinuousAt α _ x γ _ _ _ δᵒᵈ _ _ _ g f hg hf gmon
Antitone Continuous Composition Transforms Upper Semicontinuity to Lower Semicontinuity at a Point
Informal description
Let $f \colon \alpha \to \gamma$ be a function that is upper semicontinuous at a point $x \in \alpha$, and let $g \colon \gamma \to \delta$ be a function that is continuous at $f(x)$. If $g$ is antitone (i.e., order-reversing), then the composition $g \circ f$ is lower semicontinuous at $x$.
Continuous.comp_upperSemicontinuousOn_antitone theorem
{g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : UpperSemicontinuousOn f s) (gmon : Antitone g) : LowerSemicontinuousOn (g ∘ f) s
Full source 
theorem Continuous.comp_upperSemicontinuousOn_antitone {g : γ → δ} {f : α → γ} (hg : Continuous g)
    (hf : UpperSemicontinuousOn f s) (gmon : Antitone g) : LowerSemicontinuousOn (g ∘ f) s :=
  fun x hx => hg.continuousAt.comp_upperSemicontinuousWithinAt_antitone (hf x hx) gmon
Antitone Continuous Composition Transforms Upper Semicontinuity to Lower Semicontinuity on a Set
Informal description
Let $f \colon \alpha \to \gamma$ be an upper semicontinuous function on a set $s \subseteq \alpha$, and let $g \colon \gamma \to \delta$ be a continuous function. If $g$ is antitone (order-reversing), then the composition $g \circ f$ is lower semicontinuous on $s$.
Continuous.comp_upperSemicontinuous_antitone theorem
{g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : UpperSemicontinuous f) (gmon : Antitone g) : LowerSemicontinuous (g ∘ f)
Full source 
theorem Continuous.comp_upperSemicontinuous_antitone {g : γ → δ} {f : α → γ} (hg : Continuous g)
    (hf : UpperSemicontinuous f) (gmon : Antitone g) : LowerSemicontinuous (g ∘ f) := fun x =>
  hg.continuousAt.comp_upperSemicontinuousAt_antitone (hf x) gmon
Antitone Continuous Composition Transforms Upper Semicontinuity to Lower Semicontinuity
Informal description
Let $f \colon \alpha \to \gamma$ be an upper semicontinuous function between topological spaces, and let $g \colon \gamma \to \delta$ be a continuous function. If $g$ is antitone (i.e., order-reversing), then the composition $g \circ f$ is lower semicontinuous.
UpperSemicontinuousAt.comp_continuousAt theorem
{f : α → β} {g : ι → α} {x : ι} (hf : UpperSemicontinuousAt f (g x)) (hg : ContinuousAt g x) : UpperSemicontinuousAt (fun x ↦ f (g x)) x
Full source 
theorem UpperSemicontinuousAt.comp_continuousAt {f : α → β} {g : ι → α} {x : ι}
    (hf : UpperSemicontinuousAt f (g x)) (hg : ContinuousAt g x) :
    UpperSemicontinuousAt (fun x ↦ f (g x)) x :=
  fun _ lt ↦ hg.eventually (hf _ lt)
Composition of Upper Semicontinuous Function with Continuous Function Preserves Upper Semicontinuity at a Point
Informal description
Let $f \colon \alpha \to \beta$ be a function between a topological space $\alpha$ and a preordered space $\beta$, and let $g \colon \iota \to \alpha$ be a function between topological spaces. If $f$ is upper semicontinuous at $g(x)$ and $g$ is continuous at $x$, then the composition $f \circ g$ is upper semicontinuous at $x$.
UpperSemicontinuousAt.comp_continuousAt_of_eq theorem
{f : α → β} {g : ι → α} {y : α} {x : ι} (hf : UpperSemicontinuousAt f y) (hg : ContinuousAt g x) (hy : g x = y) : UpperSemicontinuousAt (fun x ↦ f (g x)) x
Full source 
theorem UpperSemicontinuousAt.comp_continuousAt_of_eq {f : α → β} {g : ι → α} {y : α} {x : ι}
    (hf : UpperSemicontinuousAt f y) (hg : ContinuousAt g x) (hy : g x = y) :
    UpperSemicontinuousAt (fun x ↦ f (g x)) x := by
  rw [← hy] at hf
  exact comp_continuousAt hf hg
Composition of Upper Semicontinuous Function with Continuous Function at Equal Point Preserves Upper Semicontinuity
Informal description
Let $f \colon \alpha \to \beta$ be a function between a topological space $\alpha$ and a preordered space $\beta$, and let $g \colon \iota \to \alpha$ be a function between topological spaces. If $f$ is upper semicontinuous at $y$, $g$ is continuous at $x$, and $g(x) = y$, then the composition $x \mapsto f(g(x))$ is upper semicontinuous at $x$.
UpperSemicontinuous.comp_continuous theorem
{f : α → β} {g : ι → α} (hf : UpperSemicontinuous f) (hg : Continuous g) : UpperSemicontinuous fun x ↦ f (g x)
Full source 
theorem UpperSemicontinuous.comp_continuous {f : α → β} {g : ι → α}
    (hf : UpperSemicontinuous f) (hg : Continuous g) : UpperSemicontinuous fun x ↦ f (g x) :=
  fun x ↦ (hf (g x)).comp_continuousAt hg.continuousAt
Composition of Upper Semicontinuous Function with Continuous Function Preserves Upper Semicontinuity
Informal description
Let $f \colon \alpha \to \beta$ be an upper semicontinuous function between a topological space $\alpha$ and a preordered space $\beta$, and let $g \colon \iota \to \alpha$ be a continuous function between topological spaces. Then the composition $f \circ g$ is upper semicontinuous.
UpperSemicontinuousWithinAt.add' theorem
{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
Full source 
/-- 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' {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 :=
  LowerSemicontinuousWithinAt.add' (γ := γᵒᵈ) hf hg hcont
Sum of Upper Semicontinuous Functions is Upper Semicontinuous (with Continuity Condition)
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two functions $f, g \colon \alpha \to \gamma$ that are upper semicontinuous at a point $x$ within a set $s \subseteq \alpha$, and assuming that the addition operation $+ \colon \gamma \times \gamma \to \gamma$ is continuous at the point $(f(x), g(x))$, then the sum $f + g$ is also upper semicontinuous at $x$ within $s$.
UpperSemicontinuousAt.add' theorem
{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
Full source 
/-- 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' {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 := by
  simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *
  exact hf.add' hg hcont
Sum of Upper Semicontinuous Functions at a Point (with Continuity Condition)
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two functions $f, g \colon \alpha \to \gamma$ that are upper semicontinuous at a point $x \in \alpha$, and assuming that the addition operation $+ \colon \gamma \times \gamma \to \gamma$ is continuous at the point $(f(x), g(x))$, then the sum $f + g$ is also upper semicontinuous at $x$.
UpperSemicontinuousOn.add' theorem
{f g : α → γ} (hf : UpperSemicontinuousOn f s) (hg : UpperSemicontinuousOn g s) (hcont : ∀ x ∈ s, ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) : UpperSemicontinuousOn (fun z => f z + g z) s
Full source 
/-- 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' {f g : α → γ} (hf : UpperSemicontinuousOn f s)
    (hg : UpperSemicontinuousOn g s)
    (hcont : ∀ x ∈ s, ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) :
    UpperSemicontinuousOn (fun z => f z + g z) s := fun x hx =>
  (hf x hx).add' (hg x hx) (hcont x hx)
Sum of Upper Semicontinuous Functions is Upper Semicontinuous (with Pointwise Continuity Condition)
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two functions $f, g \colon \alpha \to \gamma$ that are upper semicontinuous on a set $s \subseteq \alpha$, and assuming that for every $x \in s$, the addition operation $+ \colon \gamma \times \gamma \to \gamma$ is continuous at $(f(x), g(x))$, then the sum $f + g$ is also upper semicontinuous on $s$.
UpperSemicontinuous.add' theorem
{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
Full source 
/-- 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' {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 := fun x => (hf x).add' (hg x) (hcont x)
Sum of Upper Semicontinuous Functions is Upper Semicontinuous (with Pointwise Continuity Condition)
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two upper semicontinuous functions $f, g \colon \alpha \to \gamma$ such that for every $x \in \alpha$, the addition operation $+ \colon \gamma \times \gamma \to \gamma$ is continuous at $(f(x), g(x))$, then the sum $f + g$ is also upper semicontinuous.
UpperSemicontinuousWithinAt.add theorem
{f g : α → γ} (hf : UpperSemicontinuousWithinAt f s x) (hg : UpperSemicontinuousWithinAt g s x) : UpperSemicontinuousWithinAt (fun z => f z + g z) s x
Full source 
/-- 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.add {f g : α → γ} (hf : UpperSemicontinuousWithinAt f s x)
    (hg : UpperSemicontinuousWithinAt g s x) :
    UpperSemicontinuousWithinAt (fun z => f z + g z) s x :=
  hf.add' hg continuous_add.continuousAt
Sum of Upper Semicontinuous Functions is Upper Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two functions $f, g \colon \alpha \to \gamma$ that are upper semicontinuous at a point $x$ within a set $s \subseteq \alpha$, then the sum $f + g$ is also upper semicontinuous at $x$ within $s$.
UpperSemicontinuousAt.add theorem
{f g : α → γ} (hf : UpperSemicontinuousAt f x) (hg : UpperSemicontinuousAt g x) : UpperSemicontinuousAt (fun z => f z + g z) x
Full source 
/-- 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 {f g : α → γ} (hf : UpperSemicontinuousAt f x)
    (hg : UpperSemicontinuousAt g x) : UpperSemicontinuousAt (fun z => f z + g z) x :=
  hf.add' hg continuous_add.continuousAt
Sum of Upper Semicontinuous Functions at a Point is Upper Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two functions $f, g \colon \alpha \to \gamma$ that are upper semicontinuous at a point $x \in \alpha$, then the sum $f + g$ is also upper semicontinuous at $x$.
UpperSemicontinuousOn.add theorem
{f g : α → γ} (hf : UpperSemicontinuousOn f s) (hg : UpperSemicontinuousOn g s) : UpperSemicontinuousOn (fun z => f z + g z) s
Full source 
/-- 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 {f g : α → γ} (hf : UpperSemicontinuousOn f s)
    (hg : UpperSemicontinuousOn g s) : UpperSemicontinuousOn (fun z => f z + g z) s :=
  hf.add' hg fun _x _hx => continuous_add.continuousAt
Sum of Upper Semicontinuous Functions is Upper Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two functions $f, g \colon \alpha \to \gamma$ that are upper semicontinuous on a set $s \subseteq \alpha$, then the sum $f + g$ is also upper semicontinuous on $s$.
UpperSemicontinuous.add theorem
{f g : α → γ} (hf : UpperSemicontinuous f) (hg : UpperSemicontinuous g) : UpperSemicontinuous fun z => f z + g z
Full source 
/-- 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 {f g : α → γ} (hf : UpperSemicontinuous f)
    (hg : UpperSemicontinuous g) : UpperSemicontinuous fun z => f z + g z :=
  hf.add' hg fun _x => continuous_add.continuousAt
Sum of Upper Semicontinuous Functions is Upper Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\gamma$ be an ordered additive monoid. Given two upper semicontinuous functions $f, g \colon \alpha \to \gamma$, their sum $f + g$ is also upper semicontinuous.
upperSemicontinuousWithinAt_sum theorem
{f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) s x) : UpperSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x
Full source 
theorem upperSemicontinuousWithinAt_sum {f : ι → α → γ} {a : Finset ι}
    (ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) s x) :
    UpperSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x :=
  lowerSemicontinuousWithinAt_sum (γ := γᵒᵈ) ha
Finite Sum of Upper Semicontinuous Functions is Upper Semicontinuous Within a Set
Informal description
Let $\alpha$ be a topological space, $\gamma$ an ordered additive monoid, $s \subseteq \alpha$, and $x \in \alpha$. Given a finite index set $a$ and a family of functions $f_i : \alpha \to \gamma$ for $i \in a$, if each $f_i$ is upper semicontinuous at $x$ within $s$, then the finite sum $\sum_{i \in a} f_i$ is also upper semicontinuous at $x$ within $s$.
upperSemicontinuousAt_sum theorem
{f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, UpperSemicontinuousAt (f i) x) : UpperSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x
Full source 
theorem upperSemicontinuousAt_sum {f : ι → α → γ} {a : Finset ι}
    (ha : ∀ i ∈ a, UpperSemicontinuousAt (f i) x) :
    UpperSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x := by
  simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *
  exact upperSemicontinuousWithinAt_sum ha
Finite Sum of Upper Semicontinuous Functions is Upper Semicontinuous at a Point
Informal description
Let $\alpha$ be a topological space, $\gamma$ an ordered additive monoid, and $x \in \alpha$. Given a finite index set $a$ and a family of functions $f_i : \alpha \to \gamma$ for $i \in a$, if each $f_i$ is upper semicontinuous at $x$, then the finite sum $\sum_{i \in a} f_i$ is also upper semicontinuous at $x$.
upperSemicontinuousOn_sum theorem
{f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, UpperSemicontinuousOn (f i) s) : UpperSemicontinuousOn (fun z => ∑ i ∈ a, f i z) s
Full source 
theorem upperSemicontinuousOn_sum {f : ι → α → γ} {a : Finset ι}
    (ha : ∀ i ∈ a, UpperSemicontinuousOn (f i) s) :
    UpperSemicontinuousOn (fun z => ∑ i ∈ a, f i z) s := fun x hx =>
  upperSemicontinuousWithinAt_sum fun i hi => ha i hi x hx
Finite Sum of Upper Semicontinuous Functions is Upper Semicontinuous on a Set
Informal description
Let $\alpha$ be a topological space, $\gamma$ an ordered additive monoid, and $s \subseteq \alpha$. Given a finite index set $a$ and a family of functions $f_i : \alpha \to \gamma$ for $i \in a$, if each $f_i$ is upper semicontinuous on $s$, then the finite sum $\sum_{i \in a} f_i$ is also upper semicontinuous on $s$.
upperSemicontinuous_sum theorem
{f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, UpperSemicontinuous (f i)) : UpperSemicontinuous fun z => ∑ i ∈ a, f i z
Full source 
theorem upperSemicontinuous_sum {f : ι → α → γ} {a : Finset ι}
    (ha : ∀ i ∈ a, UpperSemicontinuous (f i)) : UpperSemicontinuous fun z => ∑ i ∈ a, f i z :=
  fun x => upperSemicontinuousAt_sum fun i hi => ha i hi x
Finite Sum of Upper Semicontinuous Functions is Upper Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\gamma$ an ordered additive monoid. Given a finite index set $a$ and a family of functions $f_i \colon \alpha \to \gamma$ for $i \in a$, if each $f_i$ is upper semicontinuous, then the finite sum $\sum_{i \in a} f_i$ is also upper semicontinuous.
upperSemicontinuousWithinAt_ciInf theorem
{f : ι → α → δ'} (bdd : ∀ᶠ y in 𝓝[s] x, BddBelow (range fun i => f i y)) (h : ∀ i, UpperSemicontinuousWithinAt (f i) s x) : UpperSemicontinuousWithinAt (fun x' => ⨅ i, f i x') s x
Full source 
theorem upperSemicontinuousWithinAt_ciInf {f : ι → α → δ'}
    (bdd : ∀ᶠ y in 𝓝[s] x, BddBelow (range fun i => f i y))
    (h : ∀ i, UpperSemicontinuousWithinAt (f i) s x) :
    UpperSemicontinuousWithinAt (fun x' => ⨅ i, f i x') s x :=
  @lowerSemicontinuousWithinAt_ciSup α _ x s ι δ'ᵒᵈ _ f bdd h
Infimum of a Family of Upper Semicontinuous Functions is Upper Semicontinuous Under Boundedness Condition
Informal description
Let $\alpha$ be a topological space and $\delta'$ a conditionally complete linear order. Consider a family of functions $f_i : \alpha \to \delta'$ indexed by $i \in \iota$, a set $s \subseteq \alpha$, and a point $x \in \alpha$. Suppose that: 1. For all $y$ in a neighborhood of $x$ within $s$, the set $\{f_i(y) \mid i \in \iota\}$ is bounded below. 2. Each $f_i$ is upper semicontinuous at $x$ within $s$. Then the function $x' \mapsto \inf_{i} f_i(x')$ is upper semicontinuous at $x$ within $s$.
upperSemicontinuousWithinAt_iInf theorem
{f : ι → α → δ} (h : ∀ i, UpperSemicontinuousWithinAt (f i) s x) : UpperSemicontinuousWithinAt (fun x' => ⨅ i, f i x') s x
Full source 
theorem upperSemicontinuousWithinAt_iInf {f : ι → α → δ}
    (h : ∀ i, UpperSemicontinuousWithinAt (f i) s x) :
    UpperSemicontinuousWithinAt (fun x' => ⨅ i, f i x') s x :=
  @lowerSemicontinuousWithinAt_iSup α _ x s ι δᵒᵈ _ f h
Infimum of Upper Semicontinuous Functions is Upper Semicontinuous Within a Set
Informal description
Let $\alpha$ be a topological space, $\delta$ a conditionally complete linear order, $s \subseteq \alpha$, and $x \in \alpha$. Given a family of functions $f_i : \alpha \to \delta$ indexed by $i \in \iota$, if each $f_i$ is upper semicontinuous at $x$ within $s$, then the function $x' \mapsto \inf_{i} f_i(x')$ is also upper semicontinuous at $x$ within $s$.
upperSemicontinuousWithinAt_biInf theorem
{p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, UpperSemicontinuousWithinAt (f i hi) s x) : UpperSemicontinuousWithinAt (fun x' => ⨅ (i) (hi), f i hi x') s x
Full source 
theorem upperSemicontinuousWithinAt_biInf {p : ι → Prop} {f : ∀ i, p i → α → δ}
    (h : ∀ i hi, UpperSemicontinuousWithinAt (f i hi) s x) :
    UpperSemicontinuousWithinAt (fun x' => ⨅ (i) (hi), f i hi x') s x :=
  upperSemicontinuousWithinAt_iInf fun i => upperSemicontinuousWithinAt_iInf fun hi => h i hi
Infimum of a Predicated Family of Upper Semicontinuous Functions is Upper Semicontinuous Within a Set
Informal description
Let $\alpha$ be a topological space, $\delta$ a conditionally complete linear order, $s \subseteq \alpha$, and $x \in \alpha$. Given a family of functions $f_i \colon \alpha \to \delta$ indexed by $i \in \iota$ with predicates $p_i$, if for each $i$ with $p_i$ the function $f_i$ is upper semicontinuous at $x$ within $s$, then the function $x' \mapsto \inf_{i, p_i} f_i(x')$ is also upper semicontinuous at $x$ within $s$.
upperSemicontinuousAt_ciInf theorem
{f : ι → α → δ'} (bdd : ∀ᶠ y in 𝓝 x, BddBelow (range fun i => f i y)) (h : ∀ i, UpperSemicontinuousAt (f i) x) : UpperSemicontinuousAt (fun x' => ⨅ i, f i x') x
Full source 
theorem upperSemicontinuousAt_ciInf {f : ι → α → δ'}
    (bdd : ∀ᶠ y in 𝓝 x, BddBelow (range fun i => f i y)) (h : ∀ i, UpperSemicontinuousAt (f i) x) :
    UpperSemicontinuousAt (fun x' => ⨅ i, f i x') x :=
  @lowerSemicontinuousAt_ciSup α _ x ι δ'ᵒᵈ _ f bdd h
Infimum of a Bounded Family of Upper Semicontinuous Functions is Upper Semicontinuous at a Point
Informal description
Let $\alpha$ be a topological space and $\delta'$ a conditionally complete linear order. Given a family of functions $f_i \colon \alpha \to \delta'$ indexed by $i \in \iota$, suppose that: 1. For all $y$ in a neighborhood of $x \in \alpha$, the set $\{f_i(y) \mid i \in \iota\}$ is bounded below. 2. Each $f_i$ is upper semicontinuous at $x$. Then the function $x' \mapsto \inf_{i} f_i(x')$ is upper semicontinuous at $x$.
upperSemicontinuousAt_iInf theorem
{f : ι → α → δ} (h : ∀ i, UpperSemicontinuousAt (f i) x) : UpperSemicontinuousAt (fun x' => ⨅ i, f i x') x
Full source 
theorem upperSemicontinuousAt_iInf {f : ι → α → δ} (h : ∀ i, UpperSemicontinuousAt (f i) x) :
    UpperSemicontinuousAt (fun x' => ⨅ i, f i x') x :=
  @lowerSemicontinuousAt_iSup α _ x ι δᵒᵈ _ f h
Pointwise Infimum of Upper Semicontinuous Functions is Upper Semicontinuous at a Point
Informal description
Let $\alpha$ be a topological space and $\delta$ a conditionally complete linear order. Given a family of functions $f_i \colon \alpha \to \delta$ indexed by $i \in \iota$, if each $f_i$ is upper semicontinuous at a point $x \in \alpha$, then the pointwise infimum function $x' \mapsto \inf_{i} f_i(x')$ is also upper semicontinuous at $x$.
upperSemicontinuousAt_biInf theorem
{p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, UpperSemicontinuousAt (f i hi) x) : UpperSemicontinuousAt (fun x' => ⨅ (i) (hi), f i hi x') x
Full source 
theorem upperSemicontinuousAt_biInf {p : ι → Prop} {f : ∀ i, p i → α → δ}
    (h : ∀ i hi, UpperSemicontinuousAt (f i hi) x) :
    UpperSemicontinuousAt (fun x' => ⨅ (i) (hi), f i hi x') x :=
  upperSemicontinuousAt_iInf fun i => upperSemicontinuousAt_iInf fun hi => h i hi
Pointwise Infimum of a Filtered Family of Upper Semicontinuous Functions is Upper Semicontinuous at a Point
Informal description
Let $\alpha$ be a topological space and $\delta$ a conditionally complete linear order. Given a family of functions $f_i \colon \alpha \to \delta$ indexed by $i \in \iota$ with predicates $p_i$, if for each $i$ with $p_i$ true, $f_i$ is upper semicontinuous at a point $x \in \alpha$, then the pointwise infimum function $x' \mapsto \inf_{\substack{i \\ p_i}} f_i(x')$ is also upper semicontinuous at $x$.
upperSemicontinuousOn_ciInf theorem
{f : ι → α → δ'} (bdd : ∀ x ∈ s, BddBelow (range fun i => f i x)) (h : ∀ i, UpperSemicontinuousOn (f i) s) : UpperSemicontinuousOn (fun x' => ⨅ i, f i x') s
Full source 
theorem upperSemicontinuousOn_ciInf {f : ι → α → δ'}
    (bdd : ∀ x ∈ s, BddBelow (range fun i => f i x)) (h : ∀ i, UpperSemicontinuousOn (f i) s) :
    UpperSemicontinuousOn (fun x' => ⨅ i, f i x') s := fun x hx =>
  upperSemicontinuousWithinAt_ciInf (eventually_nhdsWithin_of_forall bdd) fun i => h i x hx
Infimum of a Family of Upper Semicontinuous Functions is Upper Semicontinuous on a Set
Informal description
Let $\alpha$ be a topological space, $\delta'$ a conditionally complete linear order, and $s \subseteq \alpha$. Given a family of functions $f_i : \alpha \to \delta'$ indexed by $i \in \iota$, suppose that: 1. For every $x \in s$, the set $\{f_i(x) \mid i \in \iota\}$ is bounded below. 2. Each $f_i$ is upper semicontinuous on $s$. Then the function $x' \mapsto \inf_{i} f_i(x')$ is upper semicontinuous on $s$.
upperSemicontinuousOn_iInf theorem
{f : ι → α → δ} (h : ∀ i, UpperSemicontinuousOn (f i) s) : UpperSemicontinuousOn (fun x' => ⨅ i, f i x') s
Full source 
theorem upperSemicontinuousOn_iInf {f : ι → α → δ} (h : ∀ i, UpperSemicontinuousOn (f i) s) :
    UpperSemicontinuousOn (fun x' => ⨅ i, f i x') s := fun x hx =>
  upperSemicontinuousWithinAt_iInf fun i => h i x hx
Pointwise Infimum of Upper Semicontinuous Functions is Upper Semicontinuous on a Set
Informal description
Let $\alpha$ be a topological space, $\delta$ a conditionally complete linear order, and $s \subseteq \alpha$. Given a family of functions $f_i : \alpha \to \delta$ indexed by $i \in \iota$, if each $f_i$ is upper semicontinuous on $s$, then the pointwise infimum function $x' \mapsto \inf_{i} f_i(x')$ is also upper semicontinuous on $s$.
upperSemicontinuousOn_biInf theorem
{p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, UpperSemicontinuousOn (f i hi) s) : UpperSemicontinuousOn (fun x' => ⨅ (i) (hi), f i hi x') s
Full source 
theorem upperSemicontinuousOn_biInf {p : ι → Prop} {f : ∀ i, p i → α → δ}
    (h : ∀ i hi, UpperSemicontinuousOn (f i hi) s) :
    UpperSemicontinuousOn (fun x' => ⨅ (i) (hi), f i hi x') s :=
  upperSemicontinuousOn_iInf fun i => upperSemicontinuousOn_iInf fun hi => h i hi
Pointwise Infimum of a Family of Upper Semicontinuous Functions is Upper Semicontinuous on a Set
Informal description
Let $\alpha$ be a topological space, $\delta$ a conditionally complete linear order, and $s \subseteq \alpha$. Given a family of functions $f_i \colon \alpha \to \delta$ indexed by $i \in \iota$ with predicates $p_i$, if for each $i$ with $p_i$ the function $f_i$ is upper semicontinuous on $s$, then the pointwise infimum function $x' \mapsto \inf_{i, p_i} f_i(x')$ is also upper semicontinuous on $s$.
upperSemicontinuous_ciInf theorem
{f : ι → α → δ'} (bdd : ∀ x, BddBelow (range fun i => f i x)) (h : ∀ i, UpperSemicontinuous (f i)) : UpperSemicontinuous fun x' => ⨅ i, f i x'
Full source 
theorem upperSemicontinuous_ciInf {f : ι → α → δ'} (bdd : ∀ x, BddBelow (range fun i => f i x))
    (h : ∀ i, UpperSemicontinuous (f i)) : UpperSemicontinuous fun x' => ⨅ i, f i x' := fun x =>
  upperSemicontinuousAt_ciInf (Eventually.of_forall bdd) fun i => h i x
Infimum of a Bounded Family of Upper Semicontinuous Functions is Upper Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\delta'$ a conditionally complete linear order. Given a family of functions $f_i \colon \alpha \to \delta'$ indexed by $i \in \iota$, suppose that: 1. For every $x \in \alpha$, the set $\{f_i(x) \mid i \in \iota\}$ is bounded below. 2. Each $f_i$ is upper semicontinuous. Then the function $x' \mapsto \inf_{i} f_i(x')$ is upper semicontinuous.
upperSemicontinuous_iInf theorem
{f : ι → α → δ} (h : ∀ i, UpperSemicontinuous (f i)) : UpperSemicontinuous fun x' => ⨅ i, f i x'
Full source 
theorem upperSemicontinuous_iInf {f : ι → α → δ} (h : ∀ i, UpperSemicontinuous (f i)) :
    UpperSemicontinuous fun x' => ⨅ i, f i x' := fun x => upperSemicontinuousAt_iInf fun i => h i x
Pointwise Infimum of Upper Semicontinuous Functions is Upper Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\delta$ a conditionally complete linear order. Given a family of functions $f_i \colon \alpha \to \delta$ indexed by $i \in \iota$, if each $f_i$ is upper semicontinuous, then the pointwise infimum function $x' \mapsto \inf_{i} f_i(x')$ is also upper semicontinuous.
upperSemicontinuous_biInf theorem
{p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, UpperSemicontinuous (f i hi)) : UpperSemicontinuous fun x' => ⨅ (i) (hi), f i hi x'
Full source 
theorem upperSemicontinuous_biInf {p : ι → Prop} {f : ∀ i, p i → α → δ}
    (h : ∀ i hi, UpperSemicontinuous (f i hi)) :
    UpperSemicontinuous fun x' => ⨅ (i) (hi), f i hi x' :=
  upperSemicontinuous_iInf fun i => upperSemicontinuous_iInf fun hi => h i hi
Infimum of a Family of Upper Semicontinuous Functions is Upper Semicontinuous
Informal description
Let $\alpha$ be a topological space and $\delta$ a conditionally complete linear order. Given a family of functions $f_i \colon \alpha \to \delta$ indexed by $i \in \iota$ with predicates $p_i$, if for each $i$ where $p_i$ holds, the function $f_i$ is upper semicontinuous, then the pointwise infimum function $x' \mapsto \inf_{i, p_i} f_i(x')$ is also upper semicontinuous.
continuousWithinAt_iff_lower_upperSemicontinuousWithinAt theorem
{f : α → γ} : ContinuousWithinAt f s x ↔ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x
Full source 
theorem continuousWithinAt_iff_lower_upperSemicontinuousWithinAt {f : α → γ} :
    ContinuousWithinAtContinuousWithinAt f s x ↔
      LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x := by
  refine ⟨fun h => ⟨h.lowerSemicontinuousWithinAt, h.upperSemicontinuousWithinAt⟩, ?_⟩
  rintro ⟨h₁, h₂⟩
  intro v hv
  simp only [Filter.mem_map]
  by_cases Hl : ∃ l, l < f x
  · rcases exists_Ioc_subset_of_mem_nhds hv Hl with ⟨l, lfx, hl⟩
    by_cases Hu : ∃ u, f x < u
    · rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
      filter_upwards [h₁ l lfx, h₂ u fxu] with a lfa fau
      rcases le_or_gt (f a) (f x) with h | h
      · exact hl ⟨lfa, h⟩
      · exact hu ⟨le_of_lt h, fau⟩
    · simp only [not_exists, not_lt] at Hu
      filter_upwards [h₁ l lfx] with a lfa using hl ⟨lfa, Hu (f a)⟩
  · simp only [not_exists, not_lt] at Hl
    by_cases Hu : ∃ u, f x < u
    · rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
      filter_upwards [h₂ u fxu] with a lfa
      apply hu
      exact ⟨Hl (f a), lfa⟩
    · simp only [not_exists, not_lt] at Hu
      apply Filter.Eventually.of_forall
      intro a
      have : f a = f x := le_antisymm (Hu _) (Hl _)
      rw [this]
      exact mem_of_mem_nhds hv
Characterization of Continuity via Semicontinuity at a Point within a Set
Informal description
A function $f \colon \alpha \to \gamma$ between topological spaces is continuous at a point $x \in \alpha$ within a set $s \subseteq \alpha$ if and only if it is both lower semicontinuous and upper semicontinuous at $x$ within $s$. Here: - Lower semicontinuity at $x$ within $s$ means that for every $y < f(x)$, there exists a neighborhood $U$ of $x$ in $s$ such that $y < f(x')$ for all $x' \in U$. - Upper semicontinuity at $x$ within $s$ means that for every $y > f(x)$, there exists a neighborhood $U$ of $x$ in $s$ such that $f(x') < y$ for all $x' \in U$.
continuousAt_iff_lower_upperSemicontinuousAt theorem
{f : α → γ} : ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
Full source 
theorem continuousAt_iff_lower_upperSemicontinuousAt {f : α → γ} :
    ContinuousAtContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x := by
  simp_rw [← continuousWithinAt_univ, ← lowerSemicontinuousWithinAt_univ_iff, ←
    upperSemicontinuousWithinAt_univ_iff, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]
Characterization of Continuity via Semicontinuity at a Point
Informal description
A function $f \colon \alpha \to \gamma$ between topological spaces is continuous at a point $x \in \alpha$ if and only if it is both lower semicontinuous and upper semicontinuous at $x$.
continuousOn_iff_lower_upperSemicontinuousOn theorem
{f : α → γ} : ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
Full source 
theorem continuousOn_iff_lower_upperSemicontinuousOn {f : α → γ} :
    ContinuousOnContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s := by
  simp only [ContinuousOn, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]
  exact
    ⟨fun H => ⟨fun x hx => (H x hx).1, fun x hx => (H x hx).2⟩, fun H x hx => ⟨H.1 x hx, H.2 x hx⟩⟩
Characterization of Continuity via Semicontinuity on a Set
Informal description
A function $f \colon \alpha \to \gamma$ is continuous on a set $s \subseteq \alpha$ if and only if it is both lower semicontinuous and upper semicontinuous on $s$. Here: - Lower semicontinuity on $s$ means that for every $x \in s$ and $y < f(x)$, there exists a neighborhood of $x$ in $s$ such that $y < f(x')$ for all $x'$ in this neighborhood. - Upper semicontinuity on $s$ means that for every $x \in s$ and $y > f(x)$, there exists a neighborhood of $x$ in $s$ such that $f(x') < y$ for all $x'$ in this neighborhood.
continuous_iff_lower_upperSemicontinuous theorem
{f : α → γ} : Continuous f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
Full source 
theorem continuous_iff_lower_upperSemicontinuous {f : α → γ} :
    ContinuousContinuous f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f := by
  simp_rw [continuous_iff_continuousOn_univ, continuousOn_iff_lower_upperSemicontinuousOn,
    lowerSemicontinuousOn_univ_iff, upperSemicontinuousOn_univ_iff]
Characterization of Continuous Functions via Semicontinuity
Informal description
A function $f \colon \alpha \to \gamma$ between topological spaces is continuous if and only if it is both lower semicontinuous and upper semicontinuous.