# 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 #

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

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

Equations
• = y < f x, ∀ᶠ (x' : α) in , y < f x'
Instances For
def LowerSemicontinuousOn {α : Type u_1} [] {β : Type u_2} [] (f : αβ) (s : Set α) :

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

Equations
• = xs,
Instances For
def LowerSemicontinuousAt {α : Type u_1} [] {β : Type u_2} [] (f : αβ) (x : α) :

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

Equations
• = y < f x, ∀ᶠ (x' : α) in nhds x, y < f x'
Instances For
def LowerSemicontinuous {α : Type u_1} [] {β : Type u_2} [] (f : αβ) :

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

Equations
• = ∀ (x : α),
Instances For
def UpperSemicontinuousWithinAt {α : Type u_1} [] {β : Type u_2} [] (f : αβ) (s : Set α) (x : α) :

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

Equations
• = ∀ (y : β), f x < y∀ᶠ (x' : α) in , f x' < y
Instances For
def UpperSemicontinuousOn {α : Type u_1} [] {β : Type u_2} [] (f : αβ) (s : Set α) :

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

Equations
• = xs,
Instances For
def UpperSemicontinuousAt {α : Type u_1} [] {β : Type u_2} [] (f : αβ) (x : α) :

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

Equations
• = ∀ (y : β), f x < y∀ᶠ (x' : α) in nhds x, f x' < y
Instances For
def UpperSemicontinuous {α : Type u_1} [] {β : Type u_2} [] (f : αβ) :

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

Equations
• = ∀ (x : α),
Instances For

### Lower semicontinuous functions #

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

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

#### Constants #

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

#### Indicators #

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

#### Relationship with continuity #

theorem lowerSemicontinuous_iff_isOpen_preimage {α : Type u_1} [] {β : Type u_2} [] {f : αβ} :
∀ (y : β), IsOpen (f ⁻¹' )
theorem LowerSemicontinuous.isOpen_preimage {α : Type u_1} [] {β : Type u_2} [] {f : αβ} (hf : ) (y : β) :
theorem lowerSemicontinuous_iff_isClosed_preimage {α : Type u_1} [] {γ : Type u_3} [] {f : αγ} :
∀ (y : γ), IsClosed (f ⁻¹' )
theorem LowerSemicontinuous.isClosed_preimage {α : Type u_1} [] {γ : Type u_3} [] {f : αγ} (hf : ) (y : γ) :
theorem ContinuousWithinAt.lowerSemicontinuousWithinAt {α : Type u_1} [] {x : α} {s : Set α} {γ : Type u_3} [] [] [] {f : αγ} (h : ) :
theorem ContinuousAt.lowerSemicontinuousAt {α : Type u_1} [] {x : α} {γ : Type u_3} [] [] [] {f : αγ} (h : ) :
theorem ContinuousOn.lowerSemicontinuousOn {α : Type u_1} [] {s : Set α} {γ : Type u_3} [] [] [] {f : αγ} (h : ) :
theorem Continuous.lowerSemicontinuous {α : Type u_1} [] {γ : Type u_3} [] [] [] {f : αγ} (h : ) :

#### Equivalent definitions #

theorem lowerSemicontinuousWithinAt_iff_le_liminf {α : Type u_1} [] {x : α} {s : Set α} {γ : Type u_3} [] {f : αγ} :
theorem LowerSemicontinuousWithinAt.le_liminf {α : Type u_1} [] {x : α} {s : Set α} {γ : Type u_3} [] {f : αγ} :
f x Filter.liminf f ()

Alias of the forward direction of lowerSemicontinuousWithinAt_iff_le_liminf.

theorem lowerSemicontinuousAt_iff_le_liminf {α : Type u_1} [] {x : α} {γ : Type u_3} [] {f : αγ} :
theorem LowerSemicontinuousAt.le_liminf {α : Type u_1} [] {x : α} {γ : Type u_3} [] {f : αγ} :
f x Filter.liminf f (nhds x)

Alias of the forward direction of lowerSemicontinuousAt_iff_le_liminf.

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

Alias of the forward direction of lowerSemicontinuous_iff_le_liminf.

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

Alias of the forward direction of lowerSemicontinuousOn_iff_le_liminf.

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

Alias of lowerSemicontinuous_iff_isClosed_epigraph.

theorem LowerSemicontinuous.isClosed_epigraph {α : Type u_1} [] {γ : Type u_3} [] [] [] {f : αγ} :
IsClosed {p : α × γ | f p.1 p.2}

Alias of the forward direction of lowerSemicontinuous_iff_isClosed_epigraph.

@[deprecated LowerSemicontinuous.isClosed_epigraph]
theorem LowerSemicontinuous.IsClosed_epigraph {α : Type u_1} [] {γ : Type u_3} [] [] [] {f : αγ} :
IsClosed {p : α × γ | f p.1 p.2}

Alias of the forward direction of lowerSemicontinuous_iff_isClosed_epigraph.

Alias of the forward direction of lowerSemicontinuous_iff_isClosed_epigraph.

### Composition #

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

#### Addition #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

#### Supremum #

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

#### Infinite sums #

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

### Upper semicontinuous functions #

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

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

#### Constants #

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

#### Indicators #

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

#### Relationship with continuity #

theorem upperSemicontinuous_iff_isOpen_preimage {α : Type u_1} [] {β : Type u_2} [] {f : αβ} :
∀ (y : β), IsOpen (f ⁻¹' )
theorem UpperSemicontinuous.isOpen_preimage {α : Type u_1} [] {β : Type u_2} [] {f : αβ} (hf : ) (y : β) :
theorem upperSemicontinuous_iff_isClosed_preimage {α : Type u_1} [] {γ : Type u_3} [] {f : αγ} :
∀ (y : γ), IsClosed (f ⁻¹' )
theorem UpperSemicontinuous.isClosed_preimage {α : Type u_1} [] {γ : Type u_3} [] {f : αγ} (hf : ) (y : γ) :
theorem ContinuousWithinAt.upperSemicontinuousWithinAt {α : Type u_1} [] {x : α} {s : Set α} {γ : Type u_3} [] [] [] {f : αγ} (h : ) :
theorem ContinuousAt.upperSemicontinuousAt {α : Type u_1} [] {x : α} {γ : Type u_3} [] [] [] {f : αγ} (h : ) :
theorem ContinuousOn.upperSemicontinuousOn {α : Type u_1} [] {s : Set α} {γ : Type u_3} [] [] [] {f : αγ} (h : ) :
theorem Continuous.upperSemicontinuous {α : Type u_1} [] {γ : Type u_3} [] [] [] {f : αγ} (h : ) :

#### Equivalent definitions #

theorem upperSemicontinuousWithinAt_iff_limsup_le {α : Type u_1} [] {x : α} {s : Set α} {γ : Type u_3} [] {f : αγ} :
theorem UpperSemicontinuousWithinAt.limsup_le {α : Type u_1} [] {x : α} {s : Set α} {γ : Type u_3} [] {f : αγ} :
Filter.limsup f () f x

Alias of the forward direction of upperSemicontinuousWithinAt_iff_limsup_le.

theorem upperSemicontinuousAt_iff_limsup_le {α : Type u_1} [] {x : α} {γ : Type u_3} [] {f : αγ} :
theorem UpperSemicontinuousAt.limsup_le {α : Type u_1} [] {x : α} {γ : Type u_3} [] {f : αγ} :
Filter.limsup f (nhds x) f x

Alias of the forward direction of upperSemicontinuousAt_iff_limsup_le.

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

Alias of the forward direction of upperSemicontinuous_iff_limsup_le.

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

Alias of the forward direction of upperSemicontinuousOn_iff_limsup_le.

theorem upperSemicontinuous_iff_IsClosed_hypograph {α : Type u_1} [] {γ : Type u_3} [] [] [] {f : αγ} :
IsClosed {p : α × γ | p.2 f p.1}
theorem UpperSemicontinuous.IsClosed_hypograph {α : Type u_1} [] {γ : Type u_3} [] [] [] {f : αγ} :
IsClosed {p : α × γ | p.2 f p.1}

Alias of the forward direction of upperSemicontinuous_iff_IsClosed_hypograph.

### Composition #

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

#### Addition #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

#### Infimum #

theorem upperSemicontinuousWithinAt_ciInf {α : Type u_1} [] {x : α} {s : Set α} {ι : Sort u_3} {δ' : Type u_5} {f : ιαδ'} (bdd : ∀ᶠ (y : α) in , BddBelow (Set.range fun (i : ι) => f i y)) (h : ∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x) :
UpperSemicontinuousWithinAt (fun (x' : α) => ⨅ (i : ι), f i x') s x
theorem upperSemicontinuousWithinAt_iInf {α : Type u_1} [] {x : α} {s : Set α} {ι : Sort u_3} {δ : Type u_4} {f : ιαδ} (h : ∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x) :
UpperSemicontinuousWithinAt (fun (x' : α) => ⨅ (i : ι), f i x') s x
theorem upperSemicontinuousWithinAt_biInf {α : Type u_1} [] {x : α} {s : Set α} {ι : Sort u_3} {δ : Type u_4} {p : ιProp} {f : (i : ι) → p iαδ} (h : ∀ (i : ι) (hi : p i), UpperSemicontinuousWithinAt (f i hi) s x) :
UpperSemicontinuousWithinAt (fun (x' : α) => ⨅ (i : ι), ⨅ (hi : p i), f i hi x') s x
theorem upperSemicontinuousAt_ciInf {α : Type u_1} [] {x : α} {ι : Sort u_3} {δ' : Type u_5} {f : ιαδ'} (bdd : ∀ᶠ (y : α) in nhds x, BddBelow (Set.range fun (i : ι) => f i y)) (h : ∀ (i : ι), UpperSemicontinuousAt (f i) x) :
UpperSemicontinuousAt (fun (x' : α) => ⨅ (i : ι), f i x') x
theorem upperSemicontinuousAt_iInf {α : Type u_1} [] {x : α} {ι : Sort u_3} {δ : Type u_4} {f : ιαδ} (h : ∀ (i : ι), UpperSemicontinuousAt (f i) x) :
UpperSemicontinuousAt (fun (x' : α) => ⨅ (i : ι), f i x') x
theorem upperSemicontinuousAt_biInf {α : Type u_1} [] {x : α} {ι : Sort u_3} {δ : Type u_4} {p : ιProp} {f : (i : ι) → p iαδ} (h : ∀ (i : ι) (hi : p i), UpperSemicontinuousAt (f i hi) x) :
UpperSemicontinuousAt (fun (x' : α) => ⨅ (i : ι), ⨅ (hi : p i), f i hi x') x
theorem upperSemicontinuousOn_ciInf {α : Type u_1} [] {s : Set α} {ι : Sort u_3} {δ' : Type u_5} {f : ιαδ'} (bdd : xs, BddBelow (Set.range fun (i : ι) => f i x)) (h : ∀ (i : ι), UpperSemicontinuousOn (f i) s) :
UpperSemicontinuousOn (fun (x' : α) => ⨅ (i : ι), f i x') s
theorem upperSemicontinuousOn_iInf {α : Type u_1} [] {s : Set α} {ι : Sort u_3} {δ : Type u_4} {f : ιαδ} (h : ∀ (i : ι), UpperSemicontinuousOn (f i) s) :
UpperSemicontinuousOn (fun (x' : α) => ⨅ (i : ι), f i x') s
theorem upperSemicontinuousOn_biInf {α : Type u_1} [] {s : Set α} {ι : Sort u_3} {δ : Type u_4} {p : ιProp} {f : (i : ι) → p iαδ} (h : ∀ (i : ι) (hi : p i), UpperSemicontinuousOn (f i hi) s) :
UpperSemicontinuousOn (fun (x' : α) => ⨅ (i : ι), ⨅ (hi : p i), f i hi x') s
theorem upperSemicontinuous_ciInf {α : Type u_1} [] {ι : Sort u_3} {δ' : Type u_5} {f : ιαδ'} (bdd : ∀ (x : α), BddBelow (Set.range fun (i : ι) => f i x)) (h : ∀ (i : ι), UpperSemicontinuous (f i)) :
UpperSemicontinuous fun (x' : α) => ⨅ (i : ι), f i x'
theorem upperSemicontinuous_iInf {α : Type u_1} [] {ι : Sort u_3} {δ : Type u_4} {f : ιαδ} (h : ∀ (i : ι), UpperSemicontinuous (f i)) :
UpperSemicontinuous fun (x' : α) => ⨅ (i : ι), f i x'
theorem upperSemicontinuous_biInf {α : Type u_1} [] {ι : Sort u_3} {δ : Type u_4} {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'
theorem continuousWithinAt_iff_lower_upperSemicontinuousWithinAt {α : Type u_1} [] {x : α} {s : Set α} {γ : Type u_3} [] [] [] {f : αγ} :
theorem continuousAt_iff_lower_upperSemicontinuousAt {α : Type u_1} [] {x : α} {γ : Type u_3} [] [] [] {f : αγ} :
theorem continuousOn_iff_lower_upperSemicontinuousOn {α : Type u_1} [] {s : Set α} {γ : Type u_3} [] [] [] {f : αγ} :
theorem continuous_iff_lower_upperSemicontinuous {α : Type u_1} [] {γ : Type u_3} [] [] [] {f : αγ} :