# mathlibdocumentation

topology.semicontinuous

# Semicontinuous maps #

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

Upper semicontinuous functions are defined similarly.

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

## Main definitions and results #

We introduce 4 definitions related to lower semicontinuity:

• lower_semicontinuous_within_at f s x
• lower_semicontinuous_at f x
• lower_semicontinuous_on f s
• lower_semicontinuous f

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

• constant functions are lower semicontinuous;
• indicator s (λ _, y) is lower semicontinuous when s is open and 0 ≤ y, or when s is closed and y ≤ 0;
• continuous functions are lower semicontinuous;
• 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;
• 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.

## Implementation details #

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

### Main definitions #

def lower_semicontinuous_within_at {α : Type u_1} {β : 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
• = ∀ (y : β), y < f x(∀ᶠ (x' : α) in s, y < f x')
def lower_semicontinuous_on {α : Type u_1} {β : 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
• = ∀ (x : α), x s
def lower_semicontinuous_at {α : Type u_1} {β : 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
• = ∀ (y : β), y < f x(∀ᶠ (x' : α) in nhds x, y < f x')
def lower_semicontinuous {α : Type u_1} {β : 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
• = ∀ (x : α),
def upper_semicontinuous_within_at {α : Type u_1} {β : 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
• = ∀ (y : β), f x < y(∀ᶠ (x' : α) in s, f x' < y)
def upper_semicontinuous_on {α : Type u_1} {β : 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
• = ∀ (x : α), x s
def upper_semicontinuous_at {α : Type u_1} {β : 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
• = ∀ (y : β), f x < y(∀ᶠ (x' : α) in nhds x, f x' < y)
def upper_semicontinuous {α : Type u_1} {β : 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
• = ∀ (x : α),

### Lower semicontinuous functions #

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

theorem lower_semicontinuous_within_at.mono {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} {x : α} {s t : set α} (h : x) (hst : t s) :
theorem lower_semicontinuous_within_at_univ_iff {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} {x : α} :
theorem lower_semicontinuous_at.lower_semicontinuous_within_at {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} {x : α} (s : set α) (h : x) :
theorem lower_semicontinuous_on.lower_semicontinuous_within_at {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} {x : α} {s : set α} (h : s) (hx : x s) :
theorem lower_semicontinuous_on.mono {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} {s t : set α} (h : s) (hst : t s) :
theorem lower_semicontinuous_on_univ_iff {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} :
theorem lower_semicontinuous.lower_semicontinuous_at {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} (h : lower_semicontinuous f) (x : α) :
theorem lower_semicontinuous.lower_semicontinuous_within_at {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} (h : lower_semicontinuous f) (s : set α) (x : α) :
theorem lower_semicontinuous.lower_semicontinuous_on {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} (h : lower_semicontinuous f) (s : set α) :

#### Constants #

theorem lower_semicontinuous_within_at_const {α : Type u_1} {β : Type u_2} [preorder β] {x : α} {s : set α} {z : β} :
lower_semicontinuous_within_at (λ (x : α), z) s x
theorem lower_semicontinuous_at_const {α : Type u_1} {β : Type u_2} [preorder β] {x : α} {z : β} :
lower_semicontinuous_at (λ (x : α), z) x
theorem lower_semicontinuous_on_const {α : Type u_1} {β : Type u_2} [preorder β] {s : set α} {z : β} :
lower_semicontinuous_on (λ (x : α), z) s
theorem lower_semicontinuous_const {α : Type u_1} {β : Type u_2} [preorder β] {z : β} :
lower_semicontinuous (λ (x : α), z)

#### Indicators #

theorem is_open.lower_semicontinuous_indicator {α : Type u_1} {β : Type u_2} [preorder β] {s : set α} {y : β} [has_zero β] (hs : is_open s) (hy : 0 y) :
lower_semicontinuous (s.indicator (λ (x : α), y))
theorem is_open.lower_semicontinuous_on_indicator {α : Type u_1} {β : Type u_2} [preorder β] {s t : set α} {y : β} [has_zero β] (hs : is_open s) (hy : 0 y) :
lower_semicontinuous_on (s.indicator (λ (x : α), y)) t
theorem is_open.lower_semicontinuous_at_indicator {α : Type u_1} {β : Type u_2} [preorder β] {x : α} {s : set α} {y : β} [has_zero β] (hs : is_open s) (hy : 0 y) :
lower_semicontinuous_at (s.indicator (λ (x : α), y)) x
theorem is_open.lower_semicontinuous_within_at_indicator {α : Type u_1} {β : Type u_2} [preorder β] {x : α} {s t : set α} {y : β} [has_zero β] (hs : is_open s) (hy : 0 y) :
lower_semicontinuous_within_at (s.indicator (λ (x : α), y)) t x
theorem is_closed.lower_semicontinuous_indicator {α : Type u_1} {β : Type u_2} [preorder β] {s : set α} {y : β} [has_zero β] (hs : is_closed s) (hy : y 0) :
lower_semicontinuous (s.indicator (λ (x : α), y))
theorem is_closed.lower_semicontinuous_on_indicator {α : Type u_1} {β : Type u_2} [preorder β] {s t : set α} {y : β} [has_zero β] (hs : is_closed s) (hy : y 0) :
lower_semicontinuous_on (s.indicator (λ (x : α), y)) t
theorem is_closed.lower_semicontinuous_at_indicator {α : Type u_1} {β : Type u_2} [preorder β] {x : α} {s : set α} {y : β} [has_zero β] (hs : is_closed s) (hy : y 0) :
lower_semicontinuous_at (s.indicator (λ (x : α), y)) x
theorem is_closed.lower_semicontinuous_within_at_indicator {α : Type u_1} {β : Type u_2} [preorder β] {x : α} {s t : set α} {y : β} [has_zero β] (hs : is_closed s) (hy : y 0) :
lower_semicontinuous_within_at (s.indicator (λ (x : α), y)) t x

#### Relationship with continuity #

theorem lower_semicontinuous_iff_is_open {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} :
∀ (y : β), is_open (f ⁻¹' set.Ioi y)
theorem lower_semicontinuous.is_open_preimage {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} (hf : lower_semicontinuous f) (y : β) :
theorem continuous_within_at.lower_semicontinuous_within_at {α : Type u_1} {x : α} {s : set α} {γ : Type u_3} [linear_order γ] {f : α → γ} (h : x) :
theorem continuous_at.lower_semicontinuous_at {α : Type u_1} {x : α} {γ : Type u_3} [linear_order γ] {f : α → γ} (h : x) :
theorem continuous_on.lower_semicontinuous_on {α : Type u_1} {s : set α} {γ : Type u_3} [linear_order γ] {f : α → γ} (h : s) :
theorem continuous.lower_semicontinuous {α : Type u_1} {γ : Type u_3} [linear_order γ] {f : α → γ} (h : continuous f) :

### Composition #

theorem continuous_at.comp_lower_semicontinuous_within_at {α : Type u_1} {x : α} {s : set α} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : (f x)) (hf : x) (gmon : monotone g) :
s x
theorem continuous_at.comp_lower_semicontinuous_at {α : Type u_1} {x : α} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : (f x)) (hf : x) (gmon : monotone g) :
theorem continuous.comp_lower_semicontinuous_on {α : Type u_1} {s : set α} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : continuous g) (hf : s) (gmon : monotone g) :
theorem continuous.comp_lower_semicontinuous {α : Type u_1} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : continuous g) (hf : lower_semicontinuous f) (gmon : monotone g) :
theorem continuous_at.comp_lower_semicontinuous_within_at_antitone {α : Type u_1} {x : α} {s : set α} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : (f x)) (hf : x) (gmon : antitone g) :
s x
theorem continuous_at.comp_lower_semicontinuous_at_antitone {α : Type u_1} {x : α} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : (f x)) (hf : x) (gmon : antitone g) :
theorem continuous.comp_lower_semicontinuous_on_antitone {α : Type u_1} {s : set α} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : continuous g) (hf : s) (gmon : antitone g) :
theorem continuous.comp_lower_semicontinuous_antitone {α : Type u_1} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : continuous g) (hf : lower_semicontinuous f) (gmon : antitone g) :

theorem lower_semicontinuous_within_at.add' {α : Type u_1} {x : α} {s : set α} {γ : Type u_4} {f g : α → γ} (hf : x) (hg : x) (hcont : continuous_at (λ (p : γ × γ), p.fst + p.snd) (f x, g x)) :
lower_semicontinuous_within_at (λ (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 [has_continuous_add].

theorem lower_semicontinuous_at.add' {α : Type u_1} {x : α} {γ : Type u_4} {f g : α → γ} (hf : x) (hg : x) (hcont : continuous_at (λ (p : γ × γ), p.fst + p.snd) (f x, g x)) :
lower_semicontinuous_at (λ (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 [has_continuous_add].

theorem lower_semicontinuous_on.add' {α : Type u_1} {s : set α} {γ : Type u_4} {f g : α → γ} (hf : s) (hg : s) (hcont : ∀ (x : α), x scontinuous_at (λ (p : γ × γ), p.fst + p.snd) (f x, g x)) :
lower_semicontinuous_on (λ (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 [has_continuous_add].

theorem lower_semicontinuous.add' {α : Type u_1} {γ : Type u_4} {f g : α → γ} (hf : lower_semicontinuous f) (hg : lower_semicontinuous g) (hcont : ∀ (x : α), continuous_at (λ (p : γ × γ), p.fst + p.snd) (f x, g x)) :
lower_semicontinuous (λ (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 [has_continuous_add].

theorem lower_semicontinuous_within_at.add {α : Type u_1} {x : α} {s : set α} {γ : Type u_4} {f g : α → γ} (hf : x) (hg : x) :
lower_semicontinuous_within_at (λ (z : α), f z + g z) s x

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

theorem lower_semicontinuous_at.add {α : Type u_1} {x : α} {γ : Type u_4} {f g : α → γ} (hf : x) (hg : x) :
lower_semicontinuous_at (λ (z : α), f z + g z) x

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

theorem lower_semicontinuous_on.add {α : Type u_1} {s : set α} {γ : Type u_4} {f g : α → γ} (hf : s) (hg : s) :
lower_semicontinuous_on (λ (z : α), f z + g z) s

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

theorem lower_semicontinuous.add {α : Type u_1} {γ : Type u_4} {f g : α → γ} (hf : lower_semicontinuous f) (hg : lower_semicontinuous g) :
lower_semicontinuous (λ (z : α), f z + g z)

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

theorem lower_semicontinuous_within_at_sum {α : Type u_1} {x : α} {s : set α} {ι : Type u_3} {γ : Type u_4} {f : ι → α → γ} {a : finset ι} (ha : ∀ (i : ι), i a x) :
lower_semicontinuous_within_at (λ (z : α), a.sum (λ (i : ι), f i z)) s x
theorem lower_semicontinuous_at_sum {α : Type u_1} {x : α} {ι : Type u_3} {γ : Type u_4} {f : ι → α → γ} {a : finset ι} (ha : ∀ (i : ι), i a x) :
lower_semicontinuous_at (λ (z : α), a.sum (λ (i : ι), f i z)) x
theorem lower_semicontinuous_on_sum {α : Type u_1} {s : set α} {ι : Type u_3} {γ : Type u_4} {f : ι → α → γ} {a : finset ι} (ha : ∀ (i : ι), i a s) :
lower_semicontinuous_on (λ (z : α), a.sum (λ (i : ι), f i z)) s
theorem lower_semicontinuous_sum {α : Type u_1} {ι : Type u_3} {γ : Type u_4} {f : ι → α → γ} {a : finset ι} (ha : ∀ (i : ι), i alower_semicontinuous (f i)) :
lower_semicontinuous (λ (z : α), a.sum (λ (i : ι), f i z))

#### Supremum #

theorem lower_semicontinuous_within_at_supr {α : Type u_1} {x : α} {s : set α} {ι : Sort u_3} {δ : Type u_4} {f : ι → α → δ} (h : ∀ (i : ι), x) :
lower_semicontinuous_within_at (λ (x' : α), ⨆ (i : ι), f i x') s x
theorem lower_semicontinuous_within_at_bsupr {α : Type u_1} {x : α} {s : set α} {ι : Sort u_3} {δ : Type u_4} {p : ι → Prop} {f : Π (i : ι), p iα → δ} (h : ∀ (i : ι) (hi : p i), lower_semicontinuous_within_at (f i hi) s x) :
lower_semicontinuous_within_at (λ (x' : α), ⨆ (i : ι) (hi : p i), f i hi x') s x
theorem lower_semicontinuous_at_supr {α : Type u_1} {x : α} {ι : Sort u_3} {δ : Type u_4} {f : ι → α → δ} (h : ∀ (i : ι), x) :
lower_semicontinuous_at (λ (x' : α), ⨆ (i : ι), f i x') x
theorem lower_semicontinuous_at_bsupr {α : Type u_1} {x : α} {ι : Sort u_3} {δ : Type u_4} {p : ι → Prop} {f : Π (i : ι), p iα → δ} (h : ∀ (i : ι) (hi : p i), lower_semicontinuous_at (f i hi) x) :
lower_semicontinuous_at (λ (x' : α), ⨆ (i : ι) (hi : p i), f i hi x') x
theorem lower_semicontinuous_on_supr {α : Type u_1} {s : set α} {ι : Sort u_3} {δ : Type u_4} {f : ι → α → δ} (h : ∀ (i : ι), s) :
lower_semicontinuous_on (λ (x' : α), ⨆ (i : ι), f i x') s
theorem lower_semicontinuous_on_bsupr {α : Type u_1} {s : set α} {ι : Sort u_3} {δ : Type u_4} {p : ι → Prop} {f : Π (i : ι), p iα → δ} (h : ∀ (i : ι) (hi : p i), lower_semicontinuous_on (f i hi) s) :
lower_semicontinuous_on (λ (x' : α), ⨆ (i : ι) (hi : p i), f i hi x') s
theorem lower_semicontinuous_supr {α : Type u_1} {ι : Sort u_3} {δ : Type u_4} {f : ι → α → δ} (h : ∀ (i : ι), lower_semicontinuous (f i)) :
lower_semicontinuous (λ (x' : α), ⨆ (i : ι), f i x')
theorem lower_semicontinuous_bsupr {α : Type u_1} {ι : Sort u_3} {δ : Type u_4} {p : ι → Prop} {f : Π (i : ι), p iα → δ} (h : ∀ (i : ι) (hi : p i), lower_semicontinuous (f i hi)) :
lower_semicontinuous (λ (x' : α), ⨆ (i : ι) (hi : p i), f i hi x')

#### Infinite sums #

theorem lower_semicontinuous_within_at_tsum {α : Type u_1} {x : α} {s : set α} {ι : Type u_3} {f : ι → α → ennreal} (h : ∀ (i : ι), x) :
lower_semicontinuous_within_at (λ (x' : α), ∑' (i : ι), f i x') s x
theorem lower_semicontinuous_at_tsum {α : Type u_1} {x : α} {ι : Type u_3} {f : ι → α → ennreal} (h : ∀ (i : ι), x) :
lower_semicontinuous_at (λ (x' : α), ∑' (i : ι), f i x') x
theorem lower_semicontinuous_on_tsum {α : Type u_1} {s : set α} {ι : Type u_3} {f : ι → α → ennreal} (h : ∀ (i : ι), s) :
lower_semicontinuous_on (λ (x' : α), ∑' (i : ι), f i x') s
theorem lower_semicontinuous_tsum {α : Type u_1} {ι : Type u_3} {f : ι → α → ennreal} (h : ∀ (i : ι), lower_semicontinuous (f i)) :
lower_semicontinuous (λ (x' : α), ∑' (i : ι), f i x')

### Upper semicontinuous functions #

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

theorem upper_semicontinuous_within_at.mono {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} {x : α} {s t : set α} (h : x) (hst : t s) :
theorem upper_semicontinuous_within_at_univ_iff {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} {x : α} :
theorem upper_semicontinuous_at.upper_semicontinuous_within_at {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} {x : α} (s : set α) (h : x) :
theorem upper_semicontinuous_on.upper_semicontinuous_within_at {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} {x : α} {s : set α} (h : s) (hx : x s) :
theorem upper_semicontinuous_on.mono {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} {s t : set α} (h : s) (hst : t s) :
theorem upper_semicontinuous_on_univ_iff {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} :
theorem upper_semicontinuous.upper_semicontinuous_at {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} (h : upper_semicontinuous f) (x : α) :
theorem upper_semicontinuous.upper_semicontinuous_within_at {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} (h : upper_semicontinuous f) (s : set α) (x : α) :
theorem upper_semicontinuous.upper_semicontinuous_on {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} (h : upper_semicontinuous f) (s : set α) :

#### Constants #

theorem upper_semicontinuous_within_at_const {α : Type u_1} {β : Type u_2} [preorder β] {x : α} {s : set α} {z : β} :
upper_semicontinuous_within_at (λ (x : α), z) s x
theorem upper_semicontinuous_at_const {α : Type u_1} {β : Type u_2} [preorder β] {x : α} {z : β} :
upper_semicontinuous_at (λ (x : α), z) x
theorem upper_semicontinuous_on_const {α : Type u_1} {β : Type u_2} [preorder β] {s : set α} {z : β} :
upper_semicontinuous_on (λ (x : α), z) s
theorem upper_semicontinuous_const {α : Type u_1} {β : Type u_2} [preorder β] {z : β} :
upper_semicontinuous (λ (x : α), z)

#### Indicators #

theorem is_open.upper_semicontinuous_indicator {α : Type u_1} {β : Type u_2} [preorder β] {s : set α} {y : β} [has_zero β] (hs : is_open s) (hy : y 0) :
upper_semicontinuous (s.indicator (λ (x : α), y))
theorem is_open.upper_semicontinuous_on_indicator {α : Type u_1} {β : Type u_2} [preorder β] {s t : set α} {y : β} [has_zero β] (hs : is_open s) (hy : y 0) :
upper_semicontinuous_on (s.indicator (λ (x : α), y)) t
theorem is_open.upper_semicontinuous_at_indicator {α : Type u_1} {β : Type u_2} [preorder β] {x : α} {s : set α} {y : β} [has_zero β] (hs : is_open s) (hy : y 0) :
upper_semicontinuous_at (s.indicator (λ (x : α), y)) x
theorem is_open.upper_semicontinuous_within_at_indicator {α : Type u_1} {β : Type u_2} [preorder β] {x : α} {s t : set α} {y : β} [has_zero β] (hs : is_open s) (hy : y 0) :
upper_semicontinuous_within_at (s.indicator (λ (x : α), y)) t x
theorem is_closed.upper_semicontinuous_indicator {α : Type u_1} {β : Type u_2} [preorder β] {s : set α} {y : β} [has_zero β] (hs : is_closed s) (hy : 0 y) :
upper_semicontinuous (s.indicator (λ (x : α), y))
theorem is_closed.upper_semicontinuous_on_indicator {α : Type u_1} {β : Type u_2} [preorder β] {s t : set α} {y : β} [has_zero β] (hs : is_closed s) (hy : 0 y) :
upper_semicontinuous_on (s.indicator (λ (x : α), y)) t
theorem is_closed.upper_semicontinuous_at_indicator {α : Type u_1} {β : Type u_2} [preorder β] {x : α} {s : set α} {y : β} [has_zero β] (hs : is_closed s) (hy : 0 y) :
upper_semicontinuous_at (s.indicator (λ (x : α), y)) x
theorem is_closed.upper_semicontinuous_within_at_indicator {α : Type u_1} {β : Type u_2} [preorder β] {x : α} {s t : set α} {y : β} [has_zero β] (hs : is_closed s) (hy : 0 y) :
upper_semicontinuous_within_at (s.indicator (λ (x : α), y)) t x

#### Relationship with continuity #

theorem upper_semicontinuous_iff_is_open {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} :
∀ (y : β), is_open (f ⁻¹' set.Iio y)
theorem upper_semicontinuous.is_open_preimage {α : Type u_1} {β : Type u_2} [preorder β] {f : α → β} (hf : upper_semicontinuous f) (y : β) :
theorem continuous_within_at.upper_semicontinuous_within_at {α : Type u_1} {x : α} {s : set α} {γ : Type u_3} [linear_order γ] {f : α → γ} (h : x) :
theorem continuous_at.upper_semicontinuous_at {α : Type u_1} {x : α} {γ : Type u_3} [linear_order γ] {f : α → γ} (h : x) :
theorem continuous_on.upper_semicontinuous_on {α : Type u_1} {s : set α} {γ : Type u_3} [linear_order γ] {f : α → γ} (h : s) :
theorem continuous.upper_semicontinuous {α : Type u_1} {γ : Type u_3} [linear_order γ] {f : α → γ} (h : continuous f) :

### Composition #

theorem continuous_at.comp_upper_semicontinuous_within_at {α : Type u_1} {x : α} {s : set α} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : (f x)) (hf : x) (gmon : monotone g) :
s x
theorem continuous_at.comp_upper_semicontinuous_at {α : Type u_1} {x : α} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : (f x)) (hf : x) (gmon : monotone g) :
theorem continuous.comp_upper_semicontinuous_on {α : Type u_1} {s : set α} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : continuous g) (hf : s) (gmon : monotone g) :
theorem continuous.comp_upper_semicontinuous {α : Type u_1} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : continuous g) (hf : upper_semicontinuous f) (gmon : monotone g) :
theorem continuous_at.comp_upper_semicontinuous_within_at_antitone {α : Type u_1} {x : α} {s : set α} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : (f x)) (hf : x) (gmon : antitone g) :
s x
theorem continuous_at.comp_upper_semicontinuous_at_antitone {α : Type u_1} {x : α} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : (f x)) (hf : x) (gmon : antitone g) :
theorem continuous.comp_upper_semicontinuous_on_antitone {α : Type u_1} {s : set α} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : continuous g) (hf : s) (gmon : antitone g) :
theorem continuous.comp_upper_semicontinuous_antitone {α : Type u_1} {γ : Type u_3} [linear_order γ] {δ : Type u_4} [linear_order δ] {g : γ → δ} {f : α → γ} (hg : continuous g) (hf : upper_semicontinuous f) (gmon : antitone g) :

theorem upper_semicontinuous_within_at.add' {α : Type u_1} {x : α} {s : set α} {γ : Type u_4} {f g : α → γ} (hf : x) (hg : x) (hcont : continuous_at (λ (p : γ × γ), p.fst + p.snd) (f x, g x)) :
upper_semicontinuous_within_at (λ (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 [has_continuous_add].

theorem upper_semicontinuous_at.add' {α : Type u_1} {x : α} {γ : Type u_4} {f g : α → γ} (hf : x) (hg : x) (hcont : continuous_at (λ (p : γ × γ), p.fst + p.snd) (f x, g x)) :
upper_semicontinuous_at (λ (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 [has_continuous_add].

theorem upper_semicontinuous_on.add' {α : Type u_1} {s : set α} {γ : Type u_4} {f g : α → γ} (hf : s) (hg : s) (hcont : ∀ (x : α), x scontinuous_at (λ (p : γ × γ), p.fst + p.snd) (f x, g x)) :
upper_semicontinuous_on (λ (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 [has_continuous_add].

theorem upper_semicontinuous.add' {α : Type u_1} {γ : Type u_4} {f g : α → γ} (hf : upper_semicontinuous f) (hg : upper_semicontinuous g) (hcont : ∀ (x : α), continuous_at (λ (p : γ × γ), p.fst + p.snd) (f x, g x)) :
upper_semicontinuous (λ (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 [has_continuous_add].

theorem upper_semicontinuous_within_at.add {α : Type u_1} {x : α} {s : set α} {γ : Type u_4} {f g : α → γ} (hf : x) (hg : x) :
upper_semicontinuous_within_at (λ (z : α), f z + g z) s x

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

theorem upper_semicontinuous_at.add {α : Type u_1} {x : α} {γ : Type u_4} {f g : α → γ} (hf : x) (hg : x) :
upper_semicontinuous_at (λ (z : α), f z + g z) x

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

theorem upper_semicontinuous_on.add {α : Type u_1} {s : set α} {γ : Type u_4} {f g : α → γ} (hf : s) (hg : s) :
upper_semicontinuous_on (λ (z : α), f z + g z) s

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

theorem upper_semicontinuous.add {α : Type u_1} {γ : Type u_4} {f g : α → γ} (hf : upper_semicontinuous f) (hg : upper_semicontinuous g) :
upper_semicontinuous (λ (z : α), f z + g z)

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

theorem upper_semicontinuous_within_at_sum {α : Type u_1} {x : α} {s : set α} {ι : Type u_3} {γ : Type u_4} {f : ι → α → γ} {a : finset ι} (ha : ∀ (i : ι), i a x) :
upper_semicontinuous_within_at (λ (z : α), a.sum (λ (i : ι), f i z)) s x
theorem upper_semicontinuous_at_sum {α : Type u_1} {x : α} {ι : Type u_3} {γ : Type u_4} {f : ι → α → γ} {a : finset ι} (ha : ∀ (i : ι), i a x) :
upper_semicontinuous_at (λ (z : α), a.sum (λ (i : ι), f i z)) x
theorem upper_semicontinuous_on_sum {α : Type u_1} {s : set α} {ι : Type u_3} {γ : Type u_4} {f : ι → α → γ} {a : finset ι} (ha : ∀ (i : ι), i a s) :
upper_semicontinuous_on (λ (z : α), a.sum (λ (i : ι), f i z)) s
theorem upper_semicontinuous_sum {α : Type u_1} {ι : Type u_3} {γ : Type u_4} {f : ι → α → γ} {a : finset ι} (ha : ∀ (i : ι), i aupper_semicontinuous (f i)) :
upper_semicontinuous (λ (z : α), a.sum (λ (i : ι), f i z))

#### Infimum #

theorem upper_semicontinuous_within_at_infi {α : Type u_1} {x : α} {s : set α} {ι : Sort u_3} {δ : Type u_4} {f : ι → α → δ} (h : ∀ (i : ι), x) :
upper_semicontinuous_within_at (λ (x' : α), ⨅ (i : ι), f i x') s x
theorem upper_semicontinuous_within_at_binfi {α : Type u_1} {x : α} {s : set α} {ι : Sort u_3} {δ : Type u_4} {p : ι → Prop} {f : Π (i : ι), p iα → δ} (h : ∀ (i : ι) (hi : p i), upper_semicontinuous_within_at (f i hi) s x) :
upper_semicontinuous_within_at (λ (x' : α), ⨅ (i : ι) (hi : p i), f i hi x') s x
theorem upper_semicontinuous_at_infi {α : Type u_1} {x : α} {ι : Sort u_3} {δ : Type u_4} {f : ι → α → δ} (h : ∀ (i : ι), x) :
upper_semicontinuous_at (λ (x' : α), ⨅ (i : ι), f i x') x
theorem upper_semicontinuous_at_binfi {α : Type u_1} {x : α} {ι : Sort u_3} {δ : Type u_4} {p : ι → Prop} {f : Π (i : ι), p iα → δ} (h : ∀ (i : ι) (hi : p i), upper_semicontinuous_at (f i hi) x) :
upper_semicontinuous_at (λ (x' : α), ⨅ (i : ι) (hi : p i), f i hi x') x
theorem upper_semicontinuous_on_infi {α : Type u_1} {s : set α} {ι : Sort u_3} {δ : Type u_4} {f : ι → α → δ} (h : ∀ (i : ι), s) :
upper_semicontinuous_on (λ (x' : α), ⨅ (i : ι), f i x') s
theorem upper_semicontinuous_on_binfi {α : Type u_1} {s : set α} {ι : Sort u_3} {δ : Type u_4} {p : ι → Prop} {f : Π (i : ι), p iα → δ} (h : ∀ (i : ι) (hi : p i), upper_semicontinuous_on (f i hi) s) :
upper_semicontinuous_on (λ (x' : α), ⨅ (i : ι) (hi : p i), f i hi x') s
theorem upper_semicontinuous_infi {α : Type u_1} {ι : Sort u_3} {δ : Type u_4} {f : ι → α → δ} (h : ∀ (i : ι), upper_semicontinuous (f i)) :
upper_semicontinuous (λ (x' : α), ⨅ (i : ι), f i x')
theorem upper_semicontinuous_binfi {α : Type u_1} {ι : Sort u_3} {δ : Type u_4} {p : ι → Prop} {f : Π (i : ι), p iα → δ} (h : ∀ (i : ι) (hi : p i), upper_semicontinuous (f i hi)) :
upper_semicontinuous (λ (x' : α), ⨅ (i : ι) (hi : p i), f i hi x')
theorem continuous_within_at_iff_lower_upper_semicontinuous_within_at {α : Type u_1} {x : α} {s : set α} {γ : Type u_3} [linear_order γ] {f : α → γ} :
theorem continuous_at_iff_lower_upper_semicontinuous_at {α : Type u_1} {x : α} {γ : Type u_3} [linear_order γ] {f : α → γ} :
theorem continuous_on_iff_lower_upper_semicontinuous_on {α : Type u_1} {s : set α} {γ : Type u_3} [linear_order γ] {f : α → γ} :
theorem continuous_iff_lower_upper_semicontinuous {α : Type u_1} {γ : Type u_3} [linear_order γ] {f : α → γ} :