mathlib3 documentation

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:

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

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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : Type u_2} [preorder β] {f : α β} {x : α} {s t : set α} (h : lower_semicontinuous_within_at f s x) (hst : t s) :
theorem lower_semicontinuous_on.lower_semicontinuous_within_at {α : Type u_1} [topological_space α] {β : Type u_2} [preorder β] {f : α β} {x : α} {s : set α} (h : lower_semicontinuous_on f s) (hx : x s) :
theorem lower_semicontinuous_on.mono {α : Type u_1} [topological_space α] {β : Type u_2} [preorder β] {f : α β} {s t : set α} (h : lower_semicontinuous_on f s) (hst : t s) :
theorem lower_semicontinuous.lower_semicontinuous_at {α : Type u_1} [topological_space α] {β : Type u_2} [preorder β] {f : α β} (h : lower_semicontinuous f) (x : α) :
theorem lower_semicontinuous.lower_semicontinuous_within_at {α : Type u_1} [topological_space α] {β : Type u_2} [preorder β] {f : α β} (h : lower_semicontinuous f) (s : set α) (x : α) :

Constants #

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

Indicators #

theorem is_open.lower_semicontinuous_indicator {α : Type u_1} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : Type u_2} [preorder β] {f : α β} :
theorem lower_semicontinuous.is_open_preimage {α : Type u_1} [topological_space α] {β : Type u_2} [preorder β] {f : α β} (hf : lower_semicontinuous f) (y : β) :
theorem lower_semicontinuous.is_closed_preimage {α : Type u_1} [topological_space α] {γ : Type u_3} [linear_order γ] {f : α γ} (hf : lower_semicontinuous f) (y : γ) :
theorem continuous_at.lower_semicontinuous_at {α : Type u_1} [topological_space α] {x : α} {γ : Type u_3} [linear_order γ] [topological_space γ] [order_topology γ] {f : α γ} (h : continuous_at f x) :

Composition #

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

Addition #

theorem lower_semicontinuous_within_at.add' {α : Type u_1} [topological_space α] {x : α} {s : set α} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] {f g : α γ} (hf : lower_semicontinuous_within_at f s x) (hg : lower_semicontinuous_within_at g s 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} [topological_space α] {x : α} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] {f g : α γ} (hf : lower_semicontinuous_at f x) (hg : lower_semicontinuous_at g 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} [topological_space α] {s : set α} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] {f g : α γ} (hf : lower_semicontinuous_on f s) (hg : lower_semicontinuous_on g 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} [topological_space α] {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] {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} [topological_space α] {x : α} {s : set α} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {f g : α γ} (hf : lower_semicontinuous_within_at f s x) (hg : lower_semicontinuous_within_at g s 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} [topological_space α] {x : α} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {f g : α γ} (hf : lower_semicontinuous_at f x) (hg : lower_semicontinuous_at g 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} [topological_space α] {s : set α} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {f g : α γ} (hf : lower_semicontinuous_on f s) (hg : lower_semicontinuous_on g 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.

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} [topological_space α] {x : α} {s : set α} {ι : Type u_3} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {f : ι α γ} {a : finset ι} (ha : (i : ι), i a lower_semicontinuous_within_at (f i) s x) :
lower_semicontinuous_within_at (λ (z : α), a.sum (λ (i : ι), f i z)) s x
theorem lower_semicontinuous_at_sum {α : Type u_1} [topological_space α] {x : α} {ι : Type u_3} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {f : ι α γ} {a : finset ι} (ha : (i : ι), i a lower_semicontinuous_at (f i) x) :
lower_semicontinuous_at (λ (z : α), a.sum (λ (i : ι), f i z)) x
theorem lower_semicontinuous_on_sum {α : Type u_1} [topological_space α] {s : set α} {ι : Type u_3} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {f : ι α γ} {a : finset ι} (ha : (i : ι), i a lower_semicontinuous_on (f i) s) :
lower_semicontinuous_on (λ (z : α), a.sum (λ (i : ι), f i z)) s
theorem lower_semicontinuous_sum {α : Type u_1} [topological_space α] {ι : Type u_3} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {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} [topological_space α] {x : α} {s : set α} {ι : Sort u_3} {δ' : Type u_5} [conditionally_complete_linear_order δ'] {f : ι α δ'} (bdd : ∀ᶠ (y : α) in nhds_within x s, bdd_above (set.range (λ (i : ι), f i y))) (h : (i : ι), lower_semicontinuous_within_at (f i) s x) :
lower_semicontinuous_within_at (λ (x' : α), (i : ι), f i x') s x
theorem lower_semicontinuous_within_at_supr {α : Type u_1} [topological_space α] {x : α} {s : set α} {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {f : ι α δ} (h : (i : ι), lower_semicontinuous_within_at (f i) s x) :
lower_semicontinuous_within_at (λ (x' : α), (i : ι), f i x') s x
theorem lower_semicontinuous_within_at_bsupr {α : Type u_1} [topological_space α] {x : α} {s : set α} {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {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} [topological_space α] {x : α} {ι : Sort u_3} {δ' : Type u_5} [conditionally_complete_linear_order δ'] {f : ι α δ'} (bdd : ∀ᶠ (y : α) in nhds x, bdd_above (set.range (λ (i : ι), f i y))) (h : (i : ι), lower_semicontinuous_at (f i) x) :
lower_semicontinuous_at (λ (x' : α), (i : ι), f i x') x
theorem lower_semicontinuous_at_supr {α : Type u_1} [topological_space α] {x : α} {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {f : ι α δ} (h : (i : ι), lower_semicontinuous_at (f i) x) :
lower_semicontinuous_at (λ (x' : α), (i : ι), f i x') x
theorem lower_semicontinuous_at_bsupr {α : Type u_1} [topological_space α] {x : α} {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {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} [topological_space α] {s : set α} {ι : Sort u_3} {δ' : Type u_5} [conditionally_complete_linear_order δ'] {f : ι α δ'} (bdd : (x : α), x s bdd_above (set.range (λ (i : ι), f i x))) (h : (i : ι), lower_semicontinuous_on (f i) s) :
lower_semicontinuous_on (λ (x' : α), (i : ι), f i x') s
theorem lower_semicontinuous_on_supr {α : Type u_1} [topological_space α] {s : set α} {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {f : ι α δ} (h : (i : ι), lower_semicontinuous_on (f i) s) :
lower_semicontinuous_on (λ (x' : α), (i : ι), f i x') s
theorem lower_semicontinuous_on_bsupr {α : Type u_1} [topological_space α] {s : set α} {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {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} [topological_space α] {ι : Sort u_3} {δ' : Type u_5} [conditionally_complete_linear_order δ'] {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} [topological_space α] {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {f : ι α δ} (h : (i : ι), lower_semicontinuous (f i)) :
lower_semicontinuous (λ (x' : α), (i : ι), f i x')
theorem lower_semicontinuous_bsupr {α : Type u_1} [topological_space α] {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {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} [topological_space α] {x : α} {s : set α} {ι : Type u_3} {f : ι α ennreal} (h : (i : ι), lower_semicontinuous_within_at (f i) s x) :
lower_semicontinuous_within_at (λ (x' : α), ∑' (i : ι), f i x') s x
theorem lower_semicontinuous_at_tsum {α : Type u_1} [topological_space α] {x : α} {ι : Type u_3} {f : ι α ennreal} (h : (i : ι), lower_semicontinuous_at (f i) x) :
lower_semicontinuous_at (λ (x' : α), ∑' (i : ι), f i x') x
theorem lower_semicontinuous_on_tsum {α : Type u_1} [topological_space α] {s : set α} {ι : Type u_3} {f : ι α ennreal} (h : (i : ι), lower_semicontinuous_on (f i) s) :
lower_semicontinuous_on (λ (x' : α), ∑' (i : ι), f i x') s
theorem lower_semicontinuous_tsum {α : Type u_1} [topological_space α] {ι : 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} [topological_space α] {β : Type u_2} [preorder β] {f : α β} {x : α} {s t : set α} (h : upper_semicontinuous_within_at f s x) (hst : t s) :
theorem upper_semicontinuous_on.upper_semicontinuous_within_at {α : Type u_1} [topological_space α] {β : Type u_2} [preorder β] {f : α β} {x : α} {s : set α} (h : upper_semicontinuous_on f s) (hx : x s) :
theorem upper_semicontinuous_on.mono {α : Type u_1} [topological_space α] {β : Type u_2} [preorder β] {f : α β} {s t : set α} (h : upper_semicontinuous_on f s) (hst : t s) :
theorem upper_semicontinuous.upper_semicontinuous_at {α : Type u_1} [topological_space α] {β : Type u_2} [preorder β] {f : α β} (h : upper_semicontinuous f) (x : α) :
theorem upper_semicontinuous.upper_semicontinuous_within_at {α : Type u_1} [topological_space α] {β : Type u_2} [preorder β] {f : α β} (h : upper_semicontinuous f) (s : set α) (x : α) :

Constants #

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

Indicators #

theorem is_open.upper_semicontinuous_indicator {α : Type u_1} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : 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} [topological_space α] {β : Type u_2} [preorder β] {f : α β} :
theorem upper_semicontinuous.is_open_preimage {α : Type u_1} [topological_space α] {β : Type u_2} [preorder β] {f : α β} (hf : upper_semicontinuous f) (y : β) :
theorem upper_semicontinuous.is_closed_preimage {α : Type u_1} [topological_space α] {γ : Type u_3} [linear_order γ] {f : α γ} (hf : upper_semicontinuous f) (y : γ) :
theorem continuous_at.upper_semicontinuous_at {α : Type u_1} [topological_space α] {x : α} {γ : Type u_3} [linear_order γ] [topological_space γ] [order_topology γ] {f : α γ} (h : continuous_at f x) :

Composition #

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

Addition #

theorem upper_semicontinuous_within_at.add' {α : Type u_1} [topological_space α] {x : α} {s : set α} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] {f g : α γ} (hf : upper_semicontinuous_within_at f s x) (hg : upper_semicontinuous_within_at g s 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} [topological_space α] {x : α} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] {f g : α γ} (hf : upper_semicontinuous_at f x) (hg : upper_semicontinuous_at g 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} [topological_space α] {s : set α} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] {f g : α γ} (hf : upper_semicontinuous_on f s) (hg : upper_semicontinuous_on g 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} [topological_space α] {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] {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} [topological_space α] {x : α} {s : set α} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {f g : α γ} (hf : upper_semicontinuous_within_at f s x) (hg : upper_semicontinuous_within_at g s 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} [topological_space α] {x : α} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {f g : α γ} (hf : upper_semicontinuous_at f x) (hg : upper_semicontinuous_at g 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} [topological_space α] {s : set α} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {f g : α γ} (hf : upper_semicontinuous_on f s) (hg : upper_semicontinuous_on g 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.

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} [topological_space α] {x : α} {s : set α} {ι : Type u_3} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {f : ι α γ} {a : finset ι} (ha : (i : ι), i a upper_semicontinuous_within_at (f i) s x) :
upper_semicontinuous_within_at (λ (z : α), a.sum (λ (i : ι), f i z)) s x
theorem upper_semicontinuous_at_sum {α : Type u_1} [topological_space α] {x : α} {ι : Type u_3} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {f : ι α γ} {a : finset ι} (ha : (i : ι), i a upper_semicontinuous_at (f i) x) :
upper_semicontinuous_at (λ (z : α), a.sum (λ (i : ι), f i z)) x
theorem upper_semicontinuous_on_sum {α : Type u_1} [topological_space α] {s : set α} {ι : Type u_3} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {f : ι α γ} {a : finset ι} (ha : (i : ι), i a upper_semicontinuous_on (f i) s) :
upper_semicontinuous_on (λ (z : α), a.sum (λ (i : ι), f i z)) s
theorem upper_semicontinuous_sum {α : Type u_1} [topological_space α] {ι : Type u_3} {γ : Type u_4} [linear_ordered_add_comm_monoid γ] [topological_space γ] [order_topology γ] [has_continuous_add γ] {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} [topological_space α] {x : α} {s : set α} {ι : Sort u_3} {δ' : Type u_5} [conditionally_complete_linear_order δ'] {f : ι α δ'} (bdd : ∀ᶠ (y : α) in nhds_within x s, bdd_below (set.range (λ (i : ι), f i y))) (h : (i : ι), upper_semicontinuous_within_at (f i) s x) :
upper_semicontinuous_within_at (λ (x' : α), (i : ι), f i x') s x
theorem upper_semicontinuous_within_at_infi {α : Type u_1} [topological_space α] {x : α} {s : set α} {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {f : ι α δ} (h : (i : ι), upper_semicontinuous_within_at (f i) s x) :
upper_semicontinuous_within_at (λ (x' : α), (i : ι), f i x') s x
theorem upper_semicontinuous_within_at_binfi {α : Type u_1} [topological_space α] {x : α} {s : set α} {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {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} [topological_space α] {x : α} {ι : Sort u_3} {δ' : Type u_5} [conditionally_complete_linear_order δ'] {f : ι α δ'} (bdd : ∀ᶠ (y : α) in nhds x, bdd_below (set.range (λ (i : ι), f i y))) (h : (i : ι), upper_semicontinuous_at (f i) x) :
upper_semicontinuous_at (λ (x' : α), (i : ι), f i x') x
theorem upper_semicontinuous_at_infi {α : Type u_1} [topological_space α] {x : α} {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {f : ι α δ} (h : (i : ι), upper_semicontinuous_at (f i) x) :
upper_semicontinuous_at (λ (x' : α), (i : ι), f i x') x
theorem upper_semicontinuous_at_binfi {α : Type u_1} [topological_space α] {x : α} {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {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} [topological_space α] {s : set α} {ι : Sort u_3} {δ' : Type u_5} [conditionally_complete_linear_order δ'] {f : ι α δ'} (bdd : (x : α), x s bdd_below (set.range (λ (i : ι), f i x))) (h : (i : ι), upper_semicontinuous_on (f i) s) :
upper_semicontinuous_on (λ (x' : α), (i : ι), f i x') s
theorem upper_semicontinuous_on_infi {α : Type u_1} [topological_space α] {s : set α} {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {f : ι α δ} (h : (i : ι), upper_semicontinuous_on (f i) s) :
upper_semicontinuous_on (λ (x' : α), (i : ι), f i x') s
theorem upper_semicontinuous_on_binfi {α : Type u_1} [topological_space α] {s : set α} {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {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} [topological_space α] {ι : Sort u_3} {δ' : Type u_5} [conditionally_complete_linear_order δ'] {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} [topological_space α] {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {f : ι α δ} (h : (i : ι), upper_semicontinuous (f i)) :
upper_semicontinuous (λ (x' : α), (i : ι), f i x')
theorem upper_semicontinuous_binfi {α : Type u_1} [topological_space α] {ι : Sort u_3} {δ : Type u_4} [complete_linear_order δ] {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')