# 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 cannot 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 complete linear order;
- `lowerSemicontinuous_iff_isClosed_epigraph` in a 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 #

- https://en.wikipedia.org/wiki/Closed_convex_function
- https://en.wikipedia.org/wiki/Semi-continuity

### Main definitions #

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

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

Equations

- LowerSemicontinuousWithinAt f s x = ∀ y < f x, ∀ᶠ (x' : α) in nhdsWithin x s, y < f x'

Instances For

source
def LowerSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (s : Set α) :
Prop

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

Equations

- LowerSemicontinuousOn f s = ∀ x ∈ s, LowerSemicontinuousWithinAt f s x

Instances For

source
def LowerSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (x : α) :
Prop

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

Equations

- LowerSemicontinuousAt f x = ∀ y < f x, ∀ᶠ (x' : α) in nhds x, y < f x'

Instances For

source
def LowerSemicontinuous {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) :
Prop

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

Equations

- LowerSemicontinuous f = ∀ (x : α), LowerSemicontinuousAt f x

Instances For

source
def UpperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (s : Set α) (x : α) :
Prop

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

Equations

- UpperSemicontinuousWithinAt f s x = ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhdsWithin x s, f x' < y

Instances For

source
def UpperSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (s : Set α) :
Prop

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

Equations

- UpperSemicontinuousOn f s = ∀ x ∈ s, UpperSemicontinuousWithinAt f s x

Instances For

source
def UpperSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (x : α) :
Prop

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

Equations

- UpperSemicontinuousAt f x = ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhds x, f x' < y

Instances For

source
def UpperSemicontinuous {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) :
Prop

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

Equations

- UpperSemicontinuous f = ∀ (x : α), UpperSemicontinuousAt f x

Instances For

### Lower semicontinuous functions #

#### Basic dot notation interface for lower semicontinuity #

source
theorem LowerSemicontinuousWithinAt.mono {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {x : α} {s t : Set α} (h : LowerSemicontinuousWithinAt f s x) (hst : t ⊆ s) :
LowerSemicontinuousWithinAt f t x
source
theorem LowerSemicontinuousWithinAt.congr_of_eventuallyEq {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f g : α → β} {s : Set α} {a : α} (h : LowerSemicontinuousWithinAt f s a) (has : a ∈ s) (hfg : ∀ᶠ (x : α) in nhdsWithin a s, f x = g x) :
LowerSemicontinuousWithinAt g s a
source
theorem lowerSemicontinuousWithinAt_univ_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {x : α} :
LowerSemicontinuousWithinAt f Set.univ x ↔ LowerSemicontinuousAt f x
source
theorem LowerSemicontinuousAt.lowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {x : α} (s : Set α) (h : LowerSemicontinuousAt f x) :
LowerSemicontinuousWithinAt f s x
source
theorem LowerSemicontinuousOn.lowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {x : α} {s : Set α} (h : LowerSemicontinuousOn f s) (hx : x ∈ s) :
LowerSemicontinuousWithinAt f s x
source
theorem LowerSemicontinuousOn.mono {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {s t : Set α} (h : LowerSemicontinuousOn f s) (hst : t ⊆ s) :
LowerSemicontinuousOn f t
source
theorem lowerSemicontinuousOn_univ_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} :
LowerSemicontinuousOn f Set.univ ↔ LowerSemicontinuous f
source
@[simp]
theorem lowerSemicontinuous_restrict_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {s : Set α} :
LowerSemicontinuous (s.restrict f) ↔ LowerSemicontinuousOn f s
source
theorem LowerSemicontinuous.lowerSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} (h : LowerSemicontinuous f) (x : α) :
LowerSemicontinuousAt f x
source
theorem LowerSemicontinuous.lowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} (h : LowerSemicontinuous f) (s : Set α) (x : α) :
LowerSemicontinuousWithinAt f s x
source
theorem LowerSemicontinuous.lowerSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} (h : LowerSemicontinuous f) (s : Set α) :
LowerSemicontinuousOn f s

#### Constants #

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

### lower bounds #

source
theorem LowerSemicontinuousOn.exists_isMinOn {α : Type u_3} [TopologicalSpace α] {β : Type u_4} [LinearOrder β] {f : α → β} {s : Set α} (ne_s : s.Nonempty) (hs : IsCompact s) (hf : LowerSemicontinuousOn f s) :
∃ a ∈ s, IsMinOn f s a

A lower semicontinuous function attains its lower bound on a nonempty compact set.

source
theorem LowerSemicontinuousOn.bddBelow_of_isCompact {α : Type u_3} [TopologicalSpace α] {β : Type u_4} [LinearOrder β] {f : α → β} [Nonempty β] {s : Set α} (hs : IsCompact s) (hf : LowerSemicontinuousOn f s) :
BddBelow (f '' s)

A lower semicontinuous function is bounded below on a compact set.

#### Indicators #

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

#### Relationship with continuity #

source
theorem lowerSemicontinuous_iff_isOpen_preimage {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} :
LowerSemicontinuous f ↔ ∀ (y : β), IsOpen (f ⁻¹' Set.Ioi y)
source
theorem LowerSemicontinuous.isOpen_preimage {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} (hf : LowerSemicontinuous f) (y : β) :
IsOpen (f ⁻¹' Set.Ioi y)
source
theorem lowerSemicontinuousOn_iff_preimage_Ioi {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {s : Set α} :
LowerSemicontinuousOn f s ↔ ∀ (b : β), ∃ (u : Set α), IsOpen u ∧ s ∩ f ⁻¹' Set.Ioi b = s ∩ u
source
theorem lowerSemicontinuous_iff_isClosed_preimage {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] {f : α → γ} :
LowerSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Set.Iic y)
source
theorem LowerSemicontinuous.isClosed_preimage {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] {f : α → γ} (hf : LowerSemicontinuous f) (y : γ) :
IsClosed (f ⁻¹' Set.Iic y)
source
theorem lowerSemicontinuousOn_iff_preimage_Iic {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] {f : α → γ} :
LowerSemicontinuousOn f s ↔ ∀ (b : γ), ∃ (v : Set α), IsClosed v ∧ s ∩ f ⁻¹' Set.Iic b = s ∩ v
source
theorem ContinuousWithinAt.lowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : ContinuousWithinAt f s x) :
LowerSemicontinuousWithinAt f s x
source
theorem ContinuousAt.lowerSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : ContinuousAt f x) :
LowerSemicontinuousAt f x
source
theorem ContinuousOn.lowerSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : ContinuousOn f s) :
LowerSemicontinuousOn f s
source
theorem Continuous.lowerSemicontinuous {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : Continuous f) :
LowerSemicontinuous f

#### Equivalent definitions #

source
theorem lowerSemicontinuousWithinAt_iff_le_liminf {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] {f : α → γ} :
LowerSemicontinuousWithinAt f s x ↔ f x ≤ Filter.liminf f (nhdsWithin x s)
source
theorem LowerSemicontinuousWithinAt.le_liminf {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] {f : α → γ} :
LowerSemicontinuousWithinAt f s x → f x ≤ Filter.liminf f (nhdsWithin x s)

Alias of the forward direction of `lowerSemicontinuousWithinAt_iff_le_liminf`.

source
theorem lowerSemicontinuousAt_iff_le_liminf {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [CompleteLinearOrder γ] {f : α → γ} :
LowerSemicontinuousAt f x ↔ f x ≤ Filter.liminf f (nhds x)
source
theorem LowerSemicontinuousAt.le_liminf {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [CompleteLinearOrder γ] {f : α → γ} :
LowerSemicontinuousAt f x → f x ≤ Filter.liminf f (nhds x)

Alias of the forward direction of `lowerSemicontinuousAt_iff_le_liminf`.

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

Alias of the forward direction of `lowerSemicontinuous_iff_le_liminf`.

source
theorem lowerSemicontinuousOn_iff_le_liminf {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] {f : α → γ} :
LowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ Filter.liminf f (nhdsWithin x s)
source
theorem LowerSemicontinuousOn.le_liminf {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] {f : α → γ} :
LowerSemicontinuousOn f s → ∀ x ∈ s, f x ≤ Filter.liminf f (nhdsWithin x s)

Alias of the forward direction of `lowerSemicontinuousOn_iff_le_liminf`.

source
theorem lowerSemicontinuousOn_iff_isClosed_epigraph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [ClosedIciTopology γ] {f : α → γ} {s : Set α} (hs : IsClosed s) :
LowerSemicontinuousOn f s ↔ IsClosed {p : α × γ | p.1 ∈ s ∧ f p.1 ≤ p.2}
source
theorem lowerSemicontinuous_iff_isClosed_epigraph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [ClosedIciTopology γ] {f : α → γ} :
LowerSemicontinuous f ↔ IsClosed {p : α × γ | f p.1 ≤ p.2}
source
theorem LowerSemicontinuous.isClosed_epigraph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [ClosedIciTopology γ] {f : α → γ} :
LowerSemicontinuous f → IsClosed {p : α × γ | f p.1 ≤ p.2}

Alias of the forward direction of `lowerSemicontinuous_iff_isClosed_epigraph`.

### Composition #

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

#### Addition #

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

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

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

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

source
theorem LowerSemicontinuousOn.add' {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_4} [AddCommMonoid γ] [LinearOrder γ] [IsOrderedAddMonoid γ] [TopologicalSpace γ] [OrderTopology γ] {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

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]`.

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

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

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

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

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

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

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

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

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

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

source
theorem lowerSemicontinuousWithinAt_sum {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Type u_3} {γ : Type u_4} [AddCommMonoid γ] [LinearOrder γ] [IsOrderedAddMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) s x) :
LowerSemicontinuousWithinAt (fun (z : α) => ∑ i ∈ a, f i z) s x
source
theorem lowerSemicontinuousAt_sum {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Type u_3} {γ : Type u_4} [AddCommMonoid γ] [LinearOrder γ] [IsOrderedAddMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, LowerSemicontinuousAt (f i) x) :
LowerSemicontinuousAt (fun (z : α) => ∑ i ∈ a, f i z) x
source
theorem lowerSemicontinuousOn_sum {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Type u_3} {γ : Type u_4} [AddCommMonoid γ] [LinearOrder γ] [IsOrderedAddMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, LowerSemicontinuousOn (f i) s) :
LowerSemicontinuousOn (fun (z : α) => ∑ i ∈ a, f i z) s
source
theorem lowerSemicontinuous_sum {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {γ : Type u_4} [AddCommMonoid γ] [LinearOrder γ] [IsOrderedAddMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, LowerSemicontinuous (f i)) :
LowerSemicontinuous fun (z : α) => ∑ i ∈ a, f i z

#### Supremum #

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

#### Infinite sums #

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

### Upper semicontinuous functions #

#### Basic dot notation interface for upper semicontinuity #

source
theorem UpperSemicontinuousWithinAt.mono {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {x : α} {s t : Set α} (h : UpperSemicontinuousWithinAt f s x) (hst : t ⊆ s) :
UpperSemicontinuousWithinAt f t x
source
theorem UpperSemicontinuousWithinAt.congr_of_eventuallyEq {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f g : α → β} {s : Set α} {a : α} (h : UpperSemicontinuousWithinAt f s a) (has : a ∈ s) (hfg : ∀ᶠ (x : α) in nhdsWithin a s, f x = g x) :
UpperSemicontinuousWithinAt g s a
source
theorem upperSemicontinuousWithinAt_univ_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {x : α} :
UpperSemicontinuousWithinAt f Set.univ x ↔ UpperSemicontinuousAt f x
source
theorem UpperSemicontinuousAt.upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {x : α} (s : Set α) (h : UpperSemicontinuousAt f x) :
UpperSemicontinuousWithinAt f s x
source
theorem UpperSemicontinuousOn.upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {x : α} {s : Set α} (h : UpperSemicontinuousOn f s) (hx : x ∈ s) :
UpperSemicontinuousWithinAt f s x
source
theorem UpperSemicontinuousOn.mono {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {s t : Set α} (h : UpperSemicontinuousOn f s) (hst : t ⊆ s) :
UpperSemicontinuousOn f t
source
theorem upperSemicontinuousOn_univ_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} :
UpperSemicontinuousOn f Set.univ ↔ UpperSemicontinuous f
source
theorem UpperSemicontinuous.upperSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} (h : UpperSemicontinuous f) (x : α) :
UpperSemicontinuousAt f x
source
theorem UpperSemicontinuous.upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} (h : UpperSemicontinuous f) (s : Set α) (x : α) :
UpperSemicontinuousWithinAt f s x
source
theorem UpperSemicontinuous.upperSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} (h : UpperSemicontinuous f) (s : Set α) :
UpperSemicontinuousOn f s

#### Constants #

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

### upper bounds #

source
theorem UpperSemicontinuousOn.exists_isMaxOn {α : Type u_3} [TopologicalSpace α] {β : Type u_4} [LinearOrder β] {f : α → β} {s : Set α} (ne_s : s.Nonempty) (hs : IsCompact s) (hf : UpperSemicontinuousOn f s) :
∃ a ∈ s, IsMaxOn f s a

An upper semicontinuous function attains its upper bound on a nonempty compact set.

source
theorem UpperSemicontinuousOn.bddAbove_of_isCompact {α : Type u_3} [TopologicalSpace α] {β : Type u_4} [LinearOrder β] {f : α → β} [Nonempty β] {s : Set α} (hs : IsCompact s) (hf : UpperSemicontinuousOn f s) :
BddAbove (f '' s)

An upper semicontinuous function is bounded above on a compact set.

#### Indicators #

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

#### Relationship with continuity #

source
theorem upperSemicontinuous_iff_isOpen_preimage {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} :
UpperSemicontinuous f ↔ ∀ (y : β), IsOpen (f ⁻¹' Set.Iio y)
source
theorem UpperSemicontinuous.isOpen_preimage {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} (hf : UpperSemicontinuous f) (y : β) :
IsOpen (f ⁻¹' Set.Iio y)
source
theorem upperSemicontinuous_iff_isClosed_preimage {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] {f : α → γ} :
UpperSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Set.Ici y)
source
theorem UpperSemicontinuous.isClosed_preimage {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] {f : α → γ} (hf : UpperSemicontinuous f) (y : γ) :
IsClosed (f ⁻¹' Set.Ici y)
source
theorem ContinuousWithinAt.upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : ContinuousWithinAt f s x) :
UpperSemicontinuousWithinAt f s x
source
theorem ContinuousAt.upperSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : ContinuousAt f x) :
UpperSemicontinuousAt f x
source
theorem ContinuousOn.upperSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : ContinuousOn f s) :
UpperSemicontinuousOn f s
source
theorem Continuous.upperSemicontinuous {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : Continuous f) :
UpperSemicontinuous f

#### Equivalent definitions #

source
theorem upperSemicontinuousWithinAt_iff_limsup_le {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] {f : α → γ} :
UpperSemicontinuousWithinAt f s x ↔ Filter.limsup f (nhdsWithin x s) ≤ f x
source
theorem UpperSemicontinuousWithinAt.limsup_le {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] {f : α → γ} :
UpperSemicontinuousWithinAt f s x → Filter.limsup f (nhdsWithin x s) ≤ f x

Alias of the forward direction of `upperSemicontinuousWithinAt_iff_limsup_le`.

source
theorem upperSemicontinuousAt_iff_limsup_le {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [CompleteLinearOrder γ] {f : α → γ} :
UpperSemicontinuousAt f x ↔ Filter.limsup f (nhds x) ≤ f x
source
theorem UpperSemicontinuousAt.limsup_le {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [CompleteLinearOrder γ] {f : α → γ} :
UpperSemicontinuousAt f x → Filter.limsup f (nhds x) ≤ f x

Alias of the forward direction of `upperSemicontinuousAt_iff_limsup_le`.

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

Alias of the forward direction of `upperSemicontinuous_iff_limsup_le`.

source
theorem upperSemicontinuousOn_iff_limsup_le {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] {f : α → γ} :
UpperSemicontinuousOn f s ↔ ∀ x ∈ s, Filter.limsup f (nhdsWithin x s) ≤ f x
source
theorem UpperSemicontinuousOn.limsup_le {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] {f : α → γ} :
UpperSemicontinuousOn f s → ∀ x ∈ s, Filter.limsup f (nhdsWithin x s) ≤ f x

Alias of the forward direction of `upperSemicontinuousOn_iff_limsup_le`.

source
theorem upperSemicontinuousOn_iff_isClosed_hypograph {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [ClosedIicTopology γ] {f : α → γ} (hs : IsClosed s) :
UpperSemicontinuousOn f s ↔ IsClosed {p : α × γ | p.1 ∈ s ∧ p.2 ≤ f p.1}
source
theorem upperSemicontinuous_iff_IsClosed_hypograph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [ClosedIicTopology γ] {f : α → γ} :
UpperSemicontinuous f ↔ IsClosed {p : α × γ | p.2 ≤ f p.1}
source
theorem UpperSemicontinuous.IsClosed_hypograph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [ClosedIicTopology γ] {f : α → γ} :
UpperSemicontinuous f → IsClosed {p : α × γ | p.2 ≤ f p.1}

Alias of the forward direction of `upperSemicontinuous_iff_IsClosed_hypograph`.

### Composition #

source
theorem UpperSemicontinuousWithinAt.comp {α : Type u_3} [TopologicalSpace α] {β : Type u_4} [LinearOrder β] {γ : Type u_5} [TopologicalSpace γ] {f : α → β} {g : γ → α} {s : Set α} {c : γ} {t : Set γ} (hf : UpperSemicontinuousWithinAt f s (g c)) (hg : ContinuousWithinAt g t c) (hg' : Set.MapsTo g t s) :
UpperSemicontinuousWithinAt (f ∘ g) t c
source
theorem UpperSemicontinuousAt.comp {α : Type u_3} [TopologicalSpace α] {β : Type u_4} [LinearOrder β] {γ : Type u_5} [TopologicalSpace γ] {f : α → β} {g : γ → α} {c : γ} (hf : UpperSemicontinuousAt f (g c)) (hg : ContinuousAt g c) :
UpperSemicontinuousAt (f ∘ g) c
source
theorem UpperSemicontinuousOn.comp {α : Type u_3} [TopologicalSpace α] {β : Type u_4} [LinearOrder β] {γ : Type u_5} [TopologicalSpace γ] {f : α → β} {g : γ → α} {s : Set α} {t : Set γ} (hf : UpperSemicontinuousOn f s) (hg : ContinuousOn g t) (hg' : Set.MapsTo g t s) :
UpperSemicontinuousOn (f ∘ g) t
source
theorem UpperSemicontinuous.comp {α : Type u_3} [TopologicalSpace α] {β : Type u_4} [LinearOrder β] {γ : Type u_5} [TopologicalSpace γ] {f : α → β} {g : γ → α} (hf : UpperSemicontinuous f) (hg : Continuous g) :
UpperSemicontinuous (f ∘ g)
source
@[simp]
theorem upperSemicontinuousOn_iff_restrict {α : Type u_3} [TopologicalSpace α] {β : Type u_4} [LinearOrder β] {f : α → β} {s : Set α} :
UpperSemicontinuous (s.restrict f) ↔ UpperSemicontinuousOn f s
source
theorem upperSemicontinuousOn_iff_preimage_Iio {α : Type u_3} [TopologicalSpace α] {β : Type u_4} [LinearOrder β] {f : α → β} {s : Set α} :
UpperSemicontinuousOn f s ↔ ∀ (b : β), ∃ (u : Set α), IsOpen u ∧ s ∩ f ⁻¹' Set.Iio b = s ∩ u
source
theorem upperSemicontinuousOn_iff_preimage_Ici {α : Type u_3} [TopologicalSpace α] {β : Type u_4} [LinearOrder β] {f : α → β} {s : Set α} :
UpperSemicontinuousOn f s ↔ ∀ (b : β), ∃ (v : Set α), IsClosed v ∧ s ∩ f ⁻¹' Set.Ici b = s ∩ v
source
theorem ContinuousAt.comp_upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousWithinAt f s x) (gmon : Monotone g) :
UpperSemicontinuousWithinAt (g ∘ f) s x
source
theorem ContinuousAt.comp_upperSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousAt f x) (gmon : Monotone g) :
UpperSemicontinuousAt (g ∘ f) x
source
theorem Continuous.comp_upperSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : UpperSemicontinuousOn f s) (gmon : Monotone g) :
UpperSemicontinuousOn (g ∘ f) s
source
theorem Continuous.comp_upperSemicontinuous {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : UpperSemicontinuous f) (gmon : Monotone g) :
UpperSemicontinuous (g ∘ f)
source
theorem ContinuousAt.comp_upperSemicontinuousWithinAt_antitone {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousWithinAt f s x) (gmon : Antitone g) :
LowerSemicontinuousWithinAt (g ∘ f) s x
source
theorem ContinuousAt.comp_upperSemicontinuousAt_antitone {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousAt f x) (gmon : Antitone g) :
LowerSemicontinuousAt (g ∘ f) x
source
theorem Continuous.comp_upperSemicontinuousOn_antitone {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : UpperSemicontinuousOn f s) (gmon : Antitone g) :
LowerSemicontinuousOn (g ∘ f) s
source
theorem Continuous.comp_upperSemicontinuous_antitone {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {δ : Type u_4} [LinearOrder δ] [TopologicalSpace δ] [OrderTopology δ] {g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : UpperSemicontinuous f) (gmon : Antitone g) :
LowerSemicontinuous (g ∘ f)
source
theorem UpperSemicontinuousAt.comp_continuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : α → β} {g : ι → α} {x : ι} (hf : UpperSemicontinuousAt f (g x)) (hg : ContinuousAt g x) :
UpperSemicontinuousAt (fun (x : ι) => f (g x)) x
source
theorem UpperSemicontinuousAt.comp_continuousAt_of_eq {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : α → β} {g : ι → α} {y : α} {x : ι} (hf : UpperSemicontinuousAt f y) (hg : ContinuousAt g x) (hy : g x = y) :
UpperSemicontinuousAt (fun (x : ι) => f (g x)) x
source
theorem UpperSemicontinuous.comp_continuous {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : α → β} {g : ι → α} (hf : UpperSemicontinuous f) (hg : Continuous g) :
UpperSemicontinuous fun (x : ι) => f (g x)

#### Addition #

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

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

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

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

source
theorem UpperSemicontinuousOn.add' {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_4} [AddCommMonoid γ] [LinearOrder γ] [IsOrderedAddMonoid γ] [TopologicalSpace γ] [OrderTopology γ] {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

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]`.

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

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

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

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

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

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

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

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

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

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

source
theorem upperSemicontinuousWithinAt_sum {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Type u_3} {γ : Type u_4} [AddCommMonoid γ] [LinearOrder γ] [IsOrderedAddMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) s x) :
UpperSemicontinuousWithinAt (fun (z : α) => ∑ i ∈ a, f i z) s x
source
theorem upperSemicontinuousAt_sum {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Type u_3} {γ : Type u_4} [AddCommMonoid γ] [LinearOrder γ] [IsOrderedAddMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, UpperSemicontinuousAt (f i) x) :
UpperSemicontinuousAt (fun (z : α) => ∑ i ∈ a, f i z) x
source
theorem upperSemicontinuousOn_sum {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Type u_3} {γ : Type u_4} [AddCommMonoid γ] [LinearOrder γ] [IsOrderedAddMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, UpperSemicontinuousOn (f i) s) :
UpperSemicontinuousOn (fun (z : α) => ∑ i ∈ a, f i z) s
source
theorem upperSemicontinuous_sum {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {γ : Type u_4} [AddCommMonoid γ] [LinearOrder γ] [IsOrderedAddMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, UpperSemicontinuous (f i)) :
UpperSemicontinuous fun (z : α) => ∑ i ∈ a, f i z

#### Infimum #

source
theorem UpperSemicontinuousWithinAt.inf {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [LinearOrder β] {f g : α → β} {s : Set α} {a : α} (hf : UpperSemicontinuousWithinAt f s a) (hg : UpperSemicontinuousWithinAt g s a) :
UpperSemicontinuousWithinAt (fun (x : α) => min (f x) (g x)) s a
source
theorem UpperSemicontinuousAt.inf {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [LinearOrder β] {f g : α → β} {a : α} (hf : UpperSemicontinuousAt f a) (hg : UpperSemicontinuousAt g a) :
UpperSemicontinuousAt (fun (x : α) => min (f x) (g x)) a
source
theorem UpperSemicontinuousOn.inf {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : UpperSemicontinuousOn f s) (hg : UpperSemicontinuousOn g s) :
UpperSemicontinuousOn (fun (x : α) => min (f x) (g x)) s
source
theorem UpperSemicontinuous.inf {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [LinearOrder β] {f g : α → β} (hf : UpperSemicontinuous f) (hg : UpperSemicontinuous g) :
UpperSemicontinuous fun (x : α) => min (f x) (g x)
source
theorem UpperSemicontinuousWithinAt.sup {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [LinearOrder β] {f g : α → β} {s : Set α} {a : α} (hf : UpperSemicontinuousWithinAt f s a) (hg : UpperSemicontinuousWithinAt g s a) :
UpperSemicontinuousWithinAt (fun (x : α) => max (f x) (g x)) s a
source
theorem UpperSemicontinuousAt.sup {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [LinearOrder β] {f g : α → β} {a : α} (hf : UpperSemicontinuousAt f a) (hg : UpperSemicontinuousAt g a) :
UpperSemicontinuousAt (fun (x : α) => max (f x) (g x)) a
source
theorem UpperSemicontinuousOn.sup {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : UpperSemicontinuousOn f s) (hg : UpperSemicontinuousOn g s) :
UpperSemicontinuousOn (fun (x : α) => max (f x) (g x)) s
source
theorem UpperSemicontinuous.sup {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [LinearOrder β] {f g : α → β} (hf : UpperSemicontinuous f) (hg : UpperSemicontinuous g) :
UpperSemicontinuous fun (x : α) => max (f x) (g x)
source
theorem upperSemicontinuousWithinAt_ciInf {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'} (bdd : ∀ᶠ (y : α) in nhdsWithin x s, BddBelow (Set.range fun (i : ι) => f i y)) (h : ∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x) :
UpperSemicontinuousWithinAt (fun (x' : α) => ⨅ (i : ι), f i x') s x
source
theorem upperSemicontinuousWithinAt_iInf {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {f : ι → α → δ} (h : ∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x) :
UpperSemicontinuousWithinAt (fun (x' : α) => ⨅ (i : ι), f i x') s x
source
theorem upperSemicontinuousWithinAt_biInf {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {p : ι → Prop} {f : (i : ι) → p i → α → δ} (h : ∀ (i : ι) (hi : p i), UpperSemicontinuousWithinAt (f i hi) s x) :
UpperSemicontinuousWithinAt (fun (x' : α) => ⨅ (i : ι), ⨅ (hi : p i), f i hi x') s x
source
theorem upperSemicontinuousAt_ciInf {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'} (bdd : ∀ᶠ (y : α) in nhds x, BddBelow (Set.range fun (i : ι) => f i y)) (h : ∀ (i : ι), UpperSemicontinuousAt (f i) x) :
UpperSemicontinuousAt (fun (x' : α) => ⨅ (i : ι), f i x') x
source
theorem upperSemicontinuousAt_iInf {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {f : ι → α → δ} (h : ∀ (i : ι), UpperSemicontinuousAt (f i) x) :
UpperSemicontinuousAt (fun (x' : α) => ⨅ (i : ι), f i x') x
source
theorem upperSemicontinuousAt_biInf {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {p : ι → Prop} {f : (i : ι) → p i → α → δ} (h : ∀ (i : ι) (hi : p i), UpperSemicontinuousAt (f i hi) x) :
UpperSemicontinuousAt (fun (x' : α) => ⨅ (i : ι), ⨅ (hi : p i), f i hi x') x
source
theorem upperSemicontinuousOn_ciInf {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'} (bdd : ∀ x ∈ s, BddBelow (Set.range fun (i : ι) => f i x)) (h : ∀ (i : ι), UpperSemicontinuousOn (f i) s) :
UpperSemicontinuousOn (fun (x' : α) => ⨅ (i : ι), f i x') s
source
theorem upperSemicontinuousOn_iInf {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {f : ι → α → δ} (h : ∀ (i : ι), UpperSemicontinuousOn (f i) s) :
UpperSemicontinuousOn (fun (x' : α) => ⨅ (i : ι), f i x') s
source
theorem upperSemicontinuousOn_biInf {α : Type u_1} [TopologicalSpace α] {s : Set α} {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {p : ι → Prop} {f : (i : ι) → p i → α → δ} (h : ∀ (i : ι) (hi : p i), UpperSemicontinuousOn (f i hi) s) :
UpperSemicontinuousOn (fun (x' : α) => ⨅ (i : ι), ⨅ (hi : p i), f i hi x') s
source
theorem upperSemicontinuous_ciInf {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'} (bdd : ∀ (x : α), BddBelow (Set.range fun (i : ι) => f i x)) (h : ∀ (i : ι), UpperSemicontinuous (f i)) :
UpperSemicontinuous fun (x' : α) => ⨅ (i : ι), f i x'
source
theorem upperSemicontinuous_iInf {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {f : ι → α → δ} (h : ∀ (i : ι), UpperSemicontinuous (f i)) :
UpperSemicontinuous fun (x' : α) => ⨅ (i : ι), f i x'
source
theorem upperSemicontinuous_biInf {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} {δ : Type u_4} [CompleteLinearOrder δ] {p : ι → Prop} {f : (i : ι) → p i → α → δ} (h : ∀ (i : ι) (hi : p i), UpperSemicontinuous (f i hi)) :
UpperSemicontinuous fun (x' : α) => ⨅ (i : ι), ⨅ (hi : p i), f i hi x'
source
theorem continuousWithinAt_iff_lower_upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} :
ContinuousWithinAt f s x ↔ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x
source
theorem continuousAt_iff_lower_upperSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} :
ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
source
theorem continuousOn_iff_lower_upperSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} :
ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
source
theorem continuous_iff_lower_upperSemicontinuous {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} :
Continuous f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f