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 xlower_semicontinuous_at f xlower_semicontinuous_on f slower_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 whensis open and0 ≤ y, or whensis closed andy ≤ 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}
[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
- lower_semicontinuous_within_at f s x = ∀ (y : β), y < f x → (∀ᶠ (x' : α) in nhds_within x s, y < f x')
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
- lower_semicontinuous_on f s = ∀ (x : α), x ∈ s → lower_semicontinuous_within_at f s x
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 - ε.
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
- lower_semicontinuous f = ∀ (x : α), lower_semicontinuous_at f x
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
- upper_semicontinuous_within_at f s x = ∀ (y : β), f x < y → (∀ᶠ (x' : α) in nhds_within x s, f x' < y)
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
- upper_semicontinuous_on f s = ∀ (x : α), x ∈ s → upper_semicontinuous_within_at f s x
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 + ε.
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
- upper_semicontinuous f = ∀ (x : α), upper_semicontinuous_at f x
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_within_at_univ_iff
{α : Type u_1}
[topological_space α]
{β : Type u_2}
[preorder β]
{f : α → β}
{x : α} :
theorem
lower_semicontinuous_at.lower_semicontinuous_within_at
{α : Type u_1}
[topological_space α]
{β : Type u_2}
[preorder β]
{f : α → β}
{x : α}
(s : set α)
(h : lower_semicontinuous_at f x) :
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_on_univ_iff
{α : Type u_1}
[topological_space α]
{β : Type u_2}
[preorder β]
{f : α → β} :
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 : α) :
theorem
lower_semicontinuous.lower_semicontinuous_on
{α : Type u_1}
[topological_space α]
{β : Type u_2}
[preorder β]
{f : α → β}
(h : lower_semicontinuous f)
(s : set α) :
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_iff_is_closed_preimage
{α : Type u_1}
[topological_space α]
{γ : Type u_3}
[linear_order γ]
{f : α → γ} :
theorem
lower_semicontinuous.is_closed_preimage
{α : Type u_1}
[topological_space α]
{γ : Type u_3}
[linear_order γ]
{f : α → γ}
(hf : lower_semicontinuous f)
(y : γ) :
theorem
continuous_within_at.lower_semicontinuous_within_at
{α : Type u_1}
[topological_space α]
{x : α}
{s : set α}
{γ : Type u_3}
[linear_order γ]
[topological_space γ]
[order_topology γ]
{f : α → γ}
(h : continuous_within_at f s x) :
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) :
theorem
continuous_on.lower_semicontinuous_on
{α : Type u_1}
[topological_space α]
{s : set α}
{γ : Type u_3}
[linear_order γ]
[topological_space γ]
[order_topology γ]
{f : α → γ}
(h : continuous_on f s) :
theorem
continuous.lower_semicontinuous
{α : Type u_1}
[topological_space α]
{γ : Type u_3}
[linear_order γ]
[topological_space γ]
[order_topology γ]
{f : α → γ}
(h : continuous f) :
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) :
lower_semicontinuous_within_at (g ∘ f) s x
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) :
lower_semicontinuous_at (g ∘ f) x
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) :
lower_semicontinuous_on (g ∘ f) s
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) :
lower_semicontinuous (g ∘ f)
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) :
upper_semicontinuous_within_at (g ∘ f) s x
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) :
upper_semicontinuous_at (g ∘ f) x
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) :
upper_semicontinuous_on (g ∘ f) s
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) :
upper_semicontinuous (g ∘ f)
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.
theorem
lower_semicontinuous.add
{α : Type u_1}
[topological_space α]
{γ : Type u_4}
[linear_ordered_add_comm_monoid γ]
[topological_space γ]
[order_topology γ]
[has_continuous_add γ]
{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}
[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_within_at_univ_iff
{α : Type u_1}
[topological_space α]
{β : Type u_2}
[preorder β]
{f : α → β}
{x : α} :
theorem
upper_semicontinuous_at.upper_semicontinuous_within_at
{α : Type u_1}
[topological_space α]
{β : Type u_2}
[preorder β]
{f : α → β}
{x : α}
(s : set α)
(h : upper_semicontinuous_at f x) :
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_on_univ_iff
{α : Type u_1}
[topological_space α]
{β : Type u_2}
[preorder β]
{f : α → β} :
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 : α) :
theorem
upper_semicontinuous.upper_semicontinuous_on
{α : Type u_1}
[topological_space α]
{β : Type u_2}
[preorder β]
{f : α → β}
(h : upper_semicontinuous f)
(s : set α) :
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_iff_is_closed_preimage
{α : Type u_1}
[topological_space α]
{γ : Type u_3}
[linear_order γ]
{f : α → γ} :
theorem
upper_semicontinuous.is_closed_preimage
{α : Type u_1}
[topological_space α]
{γ : Type u_3}
[linear_order γ]
{f : α → γ}
(hf : upper_semicontinuous f)
(y : γ) :
theorem
continuous_within_at.upper_semicontinuous_within_at
{α : Type u_1}
[topological_space α]
{x : α}
{s : set α}
{γ : Type u_3}
[linear_order γ]
[topological_space γ]
[order_topology γ]
{f : α → γ}
(h : continuous_within_at f s x) :
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) :
theorem
continuous_on.upper_semicontinuous_on
{α : Type u_1}
[topological_space α]
{s : set α}
{γ : Type u_3}
[linear_order γ]
[topological_space γ]
[order_topology γ]
{f : α → γ}
(h : continuous_on f s) :
theorem
continuous.upper_semicontinuous
{α : Type u_1}
[topological_space α]
{γ : Type u_3}
[linear_order γ]
[topological_space γ]
[order_topology γ]
{f : α → γ}
(h : continuous f) :
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) :
upper_semicontinuous_within_at (g ∘ f) s x
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) :
upper_semicontinuous_at (g ∘ f) x
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) :
upper_semicontinuous_on (g ∘ f) s
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) :
upper_semicontinuous (g ∘ f)
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) :
lower_semicontinuous_within_at (g ∘ f) s x
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) :
lower_semicontinuous_at (g ∘ f) x
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) :
lower_semicontinuous_on (g ∘ f) s
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) :
lower_semicontinuous (g ∘ f)
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.
theorem
upper_semicontinuous.add
{α : Type u_1}
[topological_space α]
{γ : Type u_4}
[linear_ordered_add_comm_monoid γ]
[topological_space γ]
[order_topology γ]
[has_continuous_add γ]
{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}
[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')
theorem
continuous_within_at_iff_lower_upper_semicontinuous_within_at
{α : Type u_1}
[topological_space α]
{x : α}
{s : set α}
{γ : Type u_3}
[linear_order γ]
[topological_space γ]
[order_topology γ]
{f : α → γ} :
continuous_within_at f s x ↔ lower_semicontinuous_within_at f s x ∧ upper_semicontinuous_within_at f s x
theorem
continuous_at_iff_lower_upper_semicontinuous_at
{α : Type u_1}
[topological_space α]
{x : α}
{γ : Type u_3}
[linear_order γ]
[topological_space γ]
[order_topology γ]
{f : α → γ} :
continuous_at f x ↔ lower_semicontinuous_at f x ∧ upper_semicontinuous_at f x
theorem
continuous_on_iff_lower_upper_semicontinuous_on
{α : Type u_1}
[topological_space α]
{s : set α}
{γ : Type u_3}
[linear_order γ]
[topological_space γ]
[order_topology γ]
{f : α → γ} :
continuous_on f s ↔ lower_semicontinuous_on f s ∧ upper_semicontinuous_on f s
theorem
continuous_iff_lower_upper_semicontinuous
{α : Type u_1}
[topological_space α]
{γ : Type u_3}
[linear_order γ]
[topological_space γ]
[order_topology γ]
{f : α → γ} :