mathlib3documentation

topology.semicontinuous

Semicontinuous maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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_preimage {α : 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 lower_semicontinuous_iff_is_closed_preimage {α : Type u_1} {γ : Type u_3} [linear_order γ] {f : α γ} :
(y : γ), is_closed (f ⁻¹' set.Iic y)
theorem lower_semicontinuous.is_closed_preimage {α : Type u_1} {γ : Type u_3} [linear_order γ] {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 s continuous_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 a lower_semicontinuous (f i)) :
lower_semicontinuous (λ (z : α), a.sum (λ (i : ι), f i z))

Supremum #

theorem lower_semicontinuous_within_at_csupr {α : Type u_1} {x : α} {s : set α} {ι : Sort u_3} {δ' : Type u_5} {f : ι α δ'} (bdd : ∀ᶠ (y : α) in s, bdd_above (set.range (λ (i : ι), f i y))) (h : (i : ι), x) :
lower_semicontinuous_within_at (λ (x' : α), (i : ι), f i x') s x
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_csupr {α : Type u_1} {x : α} {ι : Sort u_3} {δ' : Type u_5} {f : ι α δ'} (bdd : ∀ᶠ (y : α) in nhds x, bdd_above (set.range (λ (i : ι), f i y))) (h : (i : ι), x) :
lower_semicontinuous_at (λ (x' : α), (i : ι), f i x') 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_csupr {α : Type u_1} {s : set α} {ι : Sort u_3} {δ' : Type u_5} {f : ι α δ'} (bdd : (x : α), x s bdd_above (set.range (λ (i : ι), f i x))) (h : (i : ι), s) :
lower_semicontinuous_on (λ (x' : α), (i : ι), f i x') s
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_csupr {α : Type u_1} {ι : Sort u_3} {δ' : Type u_5} {f : ι α δ'} (bdd : (x : α), bdd_above (set.range (λ (i : ι), f i x))) (h : (i : ι), lower_semicontinuous (f i)) :
lower_semicontinuous (λ (x' : α), (i : ι), f i x')
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 : ι } (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 : ι } (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 : ι } (h : (i : ι), s) :
lower_semicontinuous_on (λ (x' : α), ∑' (i : ι), f i x') s
theorem lower_semicontinuous_tsum {α : Type u_1} {ι : Type u_3} {f : ι } (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_preimage {α : 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 upper_semicontinuous_iff_is_closed_preimage {α : Type u_1} {γ : Type u_3} [linear_order γ] {f : α γ} :
(y : γ), is_closed (f ⁻¹' set.Ici y)
theorem upper_semicontinuous.is_closed_preimage {α : Type u_1} {γ : Type u_3} [linear_order γ] {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 s continuous_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 a upper_semicontinuous (f i)) :
upper_semicontinuous (λ (z : α), a.sum (λ (i : ι), f i z))

Infimum #

theorem upper_semicontinuous_within_at_cinfi {α : Type u_1} {x : α} {s : set α} {ι : Sort u_3} {δ' : Type u_5} {f : ι α δ'} (bdd : ∀ᶠ (y : α) in s, bdd_below (set.range (λ (i : ι), f i y))) (h : (i : ι), x) :
upper_semicontinuous_within_at (λ (x' : α), (i : ι), f i x') s x
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_cinfi {α : Type u_1} {x : α} {ι : Sort u_3} {δ' : Type u_5} {f : ι α δ'} (bdd : ∀ᶠ (y : α) in nhds x, bdd_below (set.range (λ (i : ι), f i y))) (h : (i : ι), x) :
upper_semicontinuous_at (λ (x' : α), (i : ι), f i x') 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_cinfi {α : Type u_1} {s : set α} {ι : Sort u_3} {δ' : Type u_5} {f : ι α δ'} (bdd : (x : α), x s bdd_below (set.range (λ (i : ι), f i x))) (h : (i : ι), s) :
upper_semicontinuous_on (λ (x' : α), (i : ι), f i x') s
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_cinfi {α : Type u_1} {ι : Sort u_3} {δ' : Type u_5} {f : ι α δ'} (bdd : (x : α), bdd_below (set.range (λ (i : ι), f i x))) (h : (i : ι), upper_semicontinuous (f i)) :
upper_semicontinuous (λ (x' : α), (i : ι), f i x')
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 : α γ} :