Semicontinuous maps #
A function f from a topological space α to an ordered space β is lower semicontinuous at a
point x if, for any y < f x, for any x' close enough to x, one has f x' > y. In other
words, f can jump up, but it can not jump down.
Upper semicontinuous functions are defined similarly.
This file introduces these notions, and a basic API around them mimicking the API for continuous functions.
Main definitions and results #
We introduce 4 definitions related to lower semicontinuity:
LowerSemicontinuousWithinAt f s xLowerSemicontinuousAt f xLowerSemicontinuousOn f sLowerSemicontinuous 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 OrderDual.
Main definitions #
def
LowerSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
(f : α → β)
(s : Set α)
(x : α)
:
A real function f is lower semicontinuous at x within a set s if, for any ε > 0, for all
x' close enough to x in s, then f x' is at least f x - ε. We formulate this in a general
preordered space, using an arbitrary y < f x instead of f x - ε.
Equations
- LowerSemicontinuousWithinAt f s x = ∀ (y : β), y < f x → ∀ᶠ (x' : α) in nhdsWithin x s, y < f x'
Instances For
def
LowerSemicontinuousOn
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
(f : α → β)
(s : Set α)
:
A real function f is lower semicontinuous on a set s if, for any ε > 0, for any x ∈ s,
for all x' close enough to x in s, then f x' is at least f x - ε. We formulate this in
a general preordered space, using an arbitrary y < f x instead of f x - ε.
Equations
- LowerSemicontinuousOn f s = ∀ (x : α), x ∈ s → LowerSemicontinuousWithinAt f s x
Instances For
def
LowerSemicontinuousAt
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
(f : α → β)
(x : α)
:
A real function f is lower semicontinuous at x if, for any ε > 0, for all x' close
enough to x, then f x' is at least f x - ε. We formulate this in a general preordered space,
using an arbitrary y < f x instead of f x - ε.
Equations
- LowerSemicontinuousAt f x = ∀ (y : β), y < f x → ∀ᶠ (x' : α) in nhds x, y < f x'
Instances For
def
LowerSemicontinuous
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
(f : α → β)
:
A real function f is lower semicontinuous if, for any ε > 0, for any x, for all x' close
enough to x, then f x' is at least f x - ε. We formulate this in a general preordered space,
using an arbitrary y < f x instead of f x - ε.
Equations
- LowerSemicontinuous f = ∀ (x : α), LowerSemicontinuousAt f x
Instances For
def
UpperSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
(f : α → β)
(s : Set α)
(x : α)
:
A real function f is upper semicontinuous at x within a set s if, for any ε > 0, for all
x' close enough to x in s, then f x' is at most f x + ε. We formulate this in a general
preordered space, using an arbitrary y > f x instead of f x + ε.
Equations
- UpperSemicontinuousWithinAt f s x = ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhdsWithin x s, f x' < y
Instances For
def
UpperSemicontinuousOn
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
(f : α → β)
(s : Set α)
:
A real function f is upper semicontinuous on a set s if, for any ε > 0, for any x ∈ s,
for all x' close enough to x in s, then f x' is at most f x + ε. We formulate this in a
general preordered space, using an arbitrary y > f x instead of f x + ε.
Equations
- UpperSemicontinuousOn f s = ∀ (x : α), x ∈ s → UpperSemicontinuousWithinAt f s x
Instances For
def
UpperSemicontinuousAt
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
(f : α → β)
(x : α)
:
A real function f is upper semicontinuous at x if, for any ε > 0, for all x' close
enough to x, then f x' is at most f x + ε. We formulate this in a general preordered space,
using an arbitrary y > f x instead of f x + ε.
Equations
- UpperSemicontinuousAt f x = ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhds x, f x' < y
Instances For
def
UpperSemicontinuous
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
(f : α → β)
:
A real function f is upper semicontinuous if, for any ε > 0, for any x, for all x'
close enough to x, then f x' is at most f x + ε. We formulate this in a general preordered
space, using an arbitrary y > f x instead of f x + ε.
Equations
- UpperSemicontinuous f = ∀ (x : α), UpperSemicontinuousAt f x
Instances For
Lower semicontinuous functions #
Basic dot notation interface for lower semicontinuity #
theorem
LowerSemicontinuousWithinAt.mono
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
{x : α}
{s : Set α}
{t : Set α}
(h : LowerSemicontinuousWithinAt f s x)
(hst : t ⊆ s)
:
theorem
lowerSemicontinuousWithinAt_univ_iff
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
{x : α}
:
LowerSemicontinuousWithinAt f Set.univ x ↔ LowerSemicontinuousAt f x
theorem
LowerSemicontinuousAt.lowerSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
{x : α}
(s : Set α)
(h : LowerSemicontinuousAt f x)
:
theorem
LowerSemicontinuousOn.lowerSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
{x : α}
{s : Set α}
(h : LowerSemicontinuousOn f s)
(hx : x ∈ s)
:
theorem
LowerSemicontinuousOn.mono
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
{s : Set α}
{t : Set α}
(h : LowerSemicontinuousOn f s)
(hst : t ⊆ s)
:
theorem
lowerSemicontinuousOn_univ_iff
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
:
LowerSemicontinuousOn f Set.univ ↔ LowerSemicontinuous f
theorem
LowerSemicontinuous.lowerSemicontinuousAt
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
(h : LowerSemicontinuous f)
(x : α)
:
theorem
LowerSemicontinuous.lowerSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
(h : LowerSemicontinuous f)
(s : Set α)
(x : α)
:
theorem
LowerSemicontinuous.lowerSemicontinuousOn
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
(h : LowerSemicontinuous f)
(s : Set α)
:
Constants #
theorem
lowerSemicontinuousWithinAt_const
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{x : α}
{s : Set α}
{z : β}
:
LowerSemicontinuousWithinAt (fun _x => z) s x
theorem
lowerSemicontinuousAt_const
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{x : α}
{z : β}
:
LowerSemicontinuousAt (fun _x => z) x
theorem
lowerSemicontinuousOn_const
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{s : Set α}
{z : β}
:
LowerSemicontinuousOn (fun _x => z) s
theorem
lowerSemicontinuous_const
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{z : β}
:
LowerSemicontinuous fun _x => z
Indicators #
theorem
IsOpen.lowerSemicontinuous_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{s : Set α}
{y : β}
[Zero β]
(hs : IsOpen s)
(hy : 0 ≤ y)
:
LowerSemicontinuous (Set.indicator s fun _x => y)
theorem
IsOpen.lowerSemicontinuousOn_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{s : Set α}
{t : Set α}
{y : β}
[Zero β]
(hs : IsOpen s)
(hy : 0 ≤ y)
:
LowerSemicontinuousOn (Set.indicator s fun _x => y) t
theorem
IsOpen.lowerSemicontinuousAt_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{x : α}
{s : Set α}
{y : β}
[Zero β]
(hs : IsOpen s)
(hy : 0 ≤ y)
:
LowerSemicontinuousAt (Set.indicator s fun _x => y) x
theorem
IsOpen.lowerSemicontinuousWithinAt_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{x : α}
{s : Set α}
{t : Set α}
{y : β}
[Zero β]
(hs : IsOpen s)
(hy : 0 ≤ y)
:
LowerSemicontinuousWithinAt (Set.indicator s fun _x => y) t x
theorem
IsClosed.lowerSemicontinuous_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{s : Set α}
{y : β}
[Zero β]
(hs : IsClosed s)
(hy : y ≤ 0)
:
LowerSemicontinuous (Set.indicator s fun _x => y)
theorem
IsClosed.lowerSemicontinuousOn_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{s : Set α}
{t : Set α}
{y : β}
[Zero β]
(hs : IsClosed s)
(hy : y ≤ 0)
:
LowerSemicontinuousOn (Set.indicator s fun _x => y) t
theorem
IsClosed.lowerSemicontinuousAt_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{x : α}
{s : Set α}
{y : β}
[Zero β]
(hs : IsClosed s)
(hy : y ≤ 0)
:
LowerSemicontinuousAt (Set.indicator s fun _x => y) x
theorem
IsClosed.lowerSemicontinuousWithinAt_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{x : α}
{s : Set α}
{t : Set α}
{y : β}
[Zero β]
(hs : IsClosed s)
(hy : y ≤ 0)
:
LowerSemicontinuousWithinAt (Set.indicator s fun _x => y) t x
Relationship with continuity #
theorem
lowerSemicontinuous_iff_isOpen_preimage
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
:
LowerSemicontinuous f ↔ ∀ (y : β), IsOpen (f ⁻¹' Set.Ioi y)
theorem
LowerSemicontinuous.isOpen_preimage
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
(hf : LowerSemicontinuous f)
(y : β)
:
theorem
lowerSemicontinuous_iff_isClosed_preimage
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_3}
[LinearOrder γ]
{f : α → γ}
:
LowerSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Set.Iic y)
theorem
LowerSemicontinuous.isClosed_preimage
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_3}
[LinearOrder γ]
{f : α → γ}
(hf : LowerSemicontinuous f)
(y : γ)
:
theorem
ContinuousWithinAt.lowerSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : ContinuousWithinAt f s x)
:
theorem
ContinuousAt.lowerSemicontinuousAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : ContinuousAt f x)
:
theorem
ContinuousOn.lowerSemicontinuousOn
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : ContinuousOn f s)
:
theorem
Continuous.lowerSemicontinuous
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : Continuous f)
:
Composition #
theorem
ContinuousAt.comp_lowerSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : ContinuousAt g (f x))
(hf : LowerSemicontinuousWithinAt f s x)
(gmon : Monotone g)
:
LowerSemicontinuousWithinAt (g ∘ f) s x
theorem
ContinuousAt.comp_lowerSemicontinuousAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : ContinuousAt g (f x))
(hf : LowerSemicontinuousAt f x)
(gmon : Monotone g)
:
LowerSemicontinuousAt (g ∘ f) x
theorem
Continuous.comp_lowerSemicontinuousOn
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : Continuous g)
(hf : LowerSemicontinuousOn f s)
(gmon : Monotone g)
:
LowerSemicontinuousOn (g ∘ f) s
theorem
Continuous.comp_lowerSemicontinuous
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : Continuous g)
(hf : LowerSemicontinuous f)
(gmon : Monotone g)
:
LowerSemicontinuous (g ∘ f)
theorem
ContinuousAt.comp_lowerSemicontinuousWithinAt_antitone
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : ContinuousAt g (f x))
(hf : LowerSemicontinuousWithinAt f s x)
(gmon : Antitone g)
:
UpperSemicontinuousWithinAt (g ∘ f) s x
theorem
ContinuousAt.comp_lowerSemicontinuousAt_antitone
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : ContinuousAt g (f x))
(hf : LowerSemicontinuousAt f x)
(gmon : Antitone g)
:
UpperSemicontinuousAt (g ∘ f) x
theorem
Continuous.comp_lowerSemicontinuousOn_antitone
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : Continuous g)
(hf : LowerSemicontinuousOn f s)
(gmon : Antitone g)
:
UpperSemicontinuousOn (g ∘ f) s
theorem
Continuous.comp_lowerSemicontinuous_antitone
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : Continuous g)
(hf : LowerSemicontinuous f)
(gmon : Antitone g)
:
UpperSemicontinuous (g ∘ f)
Addition #
theorem
LowerSemicontinuousWithinAt.add'
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
{g : α → γ}
(hf : LowerSemicontinuousWithinAt f s x)
(hg : LowerSemicontinuousWithinAt g s x)
(hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x))
:
LowerSemicontinuousWithinAt (fun z => f z + g z) s x
The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to EReal. The unprimed version of
the lemma uses [ContinuousAdd].
theorem
LowerSemicontinuousAt.add'
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
{g : α → γ}
(hf : LowerSemicontinuousAt f x)
(hg : LowerSemicontinuousAt g x)
(hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x))
:
LowerSemicontinuousAt (fun z => f z + g z) x
The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to EReal. The unprimed version of
the lemma uses [ContinuousAdd].
theorem
LowerSemicontinuousOn.add'
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
{g : α → γ}
(hf : LowerSemicontinuousOn f s)
(hg : LowerSemicontinuousOn g s)
(hcont : ∀ (x : α), x ∈ s → ContinuousAt (fun p => p.fst + p.snd) (f x, g x))
:
LowerSemicontinuousOn (fun z => f z + g z) s
The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to EReal. The unprimed version of
the lemma uses [ContinuousAdd].
theorem
LowerSemicontinuous.add'
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
{g : α → γ}
(hf : LowerSemicontinuous f)
(hg : LowerSemicontinuous g)
(hcont : ∀ (x : α), ContinuousAt (fun p => p.fst + p.snd) (f x, g x))
:
LowerSemicontinuous fun z => f z + g z
The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to EReal. The unprimed version of
the lemma uses [ContinuousAdd].
theorem
LowerSemicontinuousWithinAt.add
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : α → γ}
{g : α → γ}
(hf : LowerSemicontinuousWithinAt f s x)
(hg : LowerSemicontinuousWithinAt g s x)
:
LowerSemicontinuousWithinAt (fun z => f z + g z) s x
The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with
[ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to EReal.
theorem
LowerSemicontinuousAt.add
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : α → γ}
{g : α → γ}
(hf : LowerSemicontinuousAt f x)
(hg : LowerSemicontinuousAt g x)
:
LowerSemicontinuousAt (fun z => f z + g z) x
The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with
[ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to EReal.
theorem
LowerSemicontinuousOn.add
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : α → γ}
{g : α → γ}
(hf : LowerSemicontinuousOn f s)
(hg : LowerSemicontinuousOn g s)
:
LowerSemicontinuousOn (fun z => f z + g z) s
The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with
[ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to EReal.
theorem
LowerSemicontinuous.add
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : α → γ}
{g : α → γ}
(hf : LowerSemicontinuous f)
(hg : LowerSemicontinuous g)
:
LowerSemicontinuous fun z => f z + g z
The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with
[ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to EReal.
theorem
lowerSemicontinuousWithinAt_sum
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{ι : Type u_3}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x)
:
LowerSemicontinuousWithinAt (fun z => Finset.sum a fun i => f i z) s x
theorem
lowerSemicontinuousAt_sum
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{ι : Type u_3}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ (i : ι), i ∈ a → LowerSemicontinuousAt (f i) x)
:
LowerSemicontinuousAt (fun z => Finset.sum a fun i => f i z) x
theorem
lowerSemicontinuousOn_sum
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{ι : Type u_3}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ (i : ι), i ∈ a → LowerSemicontinuousOn (f i) s)
:
LowerSemicontinuousOn (fun z => Finset.sum a fun i => f i z) s
theorem
lowerSemicontinuous_sum
{α : Type u_1}
[TopologicalSpace α]
{ι : Type u_3}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ (i : ι), i ∈ a → LowerSemicontinuous (f i))
:
LowerSemicontinuous fun z => Finset.sum a fun i => f i z
Supremum #
theorem
lowerSemicontinuousWithinAt_ciSup
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{ι : Sort u_3}
{δ' : Type u_5}
[ConditionallyCompleteLinearOrder δ']
{f : ι → α → δ'}
(bdd : ∀ᶠ (y : α) in nhdsWithin x s, BddAbove (Set.range fun i => f i y))
(h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x)
:
LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') s x
theorem
lowerSemicontinuousWithinAt_iSup
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{f : ι → α → δ}
(h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x)
:
LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') s x
theorem
lowerSemicontinuousWithinAt_biSup
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{p : ι → Prop}
{f : (i : ι) → p i → α → δ}
(h : ∀ (i : ι) (hi : p i), LowerSemicontinuousWithinAt (f i hi) s x)
:
LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι) (hi : p i), f i hi x') s x
theorem
lowerSemicontinuousAt_ciSup
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{ι : Sort u_3}
{δ' : Type u_5}
[ConditionallyCompleteLinearOrder δ']
{f : ι → α → δ'}
(bdd : ∀ᶠ (y : α) in nhds x, BddAbove (Set.range fun i => f i y))
(h : ∀ (i : ι), LowerSemicontinuousAt (f i) x)
:
LowerSemicontinuousAt (fun x' => ⨆ (i : ι), f i x') x
theorem
lowerSemicontinuousAt_iSup
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{f : ι → α → δ}
(h : ∀ (i : ι), LowerSemicontinuousAt (f i) x)
:
LowerSemicontinuousAt (fun x' => ⨆ (i : ι), f i x') x
theorem
lowerSemicontinuousAt_biSup
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{p : ι → Prop}
{f : (i : ι) → p i → α → δ}
(h : ∀ (i : ι) (hi : p i), LowerSemicontinuousAt (f i hi) x)
:
LowerSemicontinuousAt (fun x' => ⨆ (i : ι) (hi : p i), f i hi x') x
theorem
lowerSemicontinuousOn_ciSup
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{ι : Sort u_3}
{δ' : Type u_5}
[ConditionallyCompleteLinearOrder δ']
{f : ι → α → δ'}
(bdd : ∀ (x : α), x ∈ s → BddAbove (Set.range fun i => f i x))
(h : ∀ (i : ι), LowerSemicontinuousOn (f i) s)
:
LowerSemicontinuousOn (fun x' => ⨆ (i : ι), f i x') s
theorem
lowerSemicontinuousOn_iSup
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{f : ι → α → δ}
(h : ∀ (i : ι), LowerSemicontinuousOn (f i) s)
:
LowerSemicontinuousOn (fun x' => ⨆ (i : ι), f i x') s
theorem
lowerSemicontinuousOn_biSup
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{p : ι → Prop}
{f : (i : ι) → p i → α → δ}
(h : ∀ (i : ι) (hi : p i), LowerSemicontinuousOn (f i hi) s)
:
LowerSemicontinuousOn (fun x' => ⨆ (i : ι) (hi : p i), f i hi x') s
theorem
lowerSemicontinuous_ciSup
{α : Type u_1}
[TopologicalSpace α]
{ι : Sort u_3}
{δ' : Type u_5}
[ConditionallyCompleteLinearOrder δ']
{f : ι → α → δ'}
(bdd : ∀ (x : α), BddAbove (Set.range fun i => f i x))
(h : ∀ (i : ι), LowerSemicontinuous (f i))
:
LowerSemicontinuous fun x' => ⨆ (i : ι), f i x'
theorem
lowerSemicontinuous_iSup
{α : Type u_1}
[TopologicalSpace α]
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{f : ι → α → δ}
(h : ∀ (i : ι), LowerSemicontinuous (f i))
:
LowerSemicontinuous fun x' => ⨆ (i : ι), f i x'
theorem
lowerSemicontinuous_biSup
{α : Type u_1}
[TopologicalSpace α]
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{p : ι → Prop}
{f : (i : ι) → p i → α → δ}
(h : ∀ (i : ι) (hi : p i), LowerSemicontinuous (f i hi))
:
LowerSemicontinuous fun x' => ⨆ (i : ι) (hi : p i), f i hi x'
Infinite sums #
theorem
lowerSemicontinuousWithinAt_tsum
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{ι : Type u_3}
{f : ι → α → ENNReal}
(h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x)
:
LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') s x
theorem
lowerSemicontinuousAt_tsum
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{ι : Type u_3}
{f : ι → α → ENNReal}
(h : ∀ (i : ι), LowerSemicontinuousAt (f i) x)
:
LowerSemicontinuousAt (fun x' => ∑' (i : ι), f i x') x
theorem
lowerSemicontinuousOn_tsum
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{ι : Type u_3}
{f : ι → α → ENNReal}
(h : ∀ (i : ι), LowerSemicontinuousOn (f i) s)
:
LowerSemicontinuousOn (fun x' => ∑' (i : ι), f i x') s
theorem
lowerSemicontinuous_tsum
{α : Type u_1}
[TopologicalSpace α]
{ι : Type u_3}
{f : ι → α → ENNReal}
(h : ∀ (i : ι), LowerSemicontinuous (f i))
:
LowerSemicontinuous fun x' => ∑' (i : ι), f i x'
Upper semicontinuous functions #
Basic dot notation interface for upper semicontinuity #
theorem
UpperSemicontinuousWithinAt.mono
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
{x : α}
{s : Set α}
{t : Set α}
(h : UpperSemicontinuousWithinAt f s x)
(hst : t ⊆ s)
:
theorem
upperSemicontinuousWithinAt_univ_iff
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
{x : α}
:
UpperSemicontinuousWithinAt f Set.univ x ↔ UpperSemicontinuousAt f x
theorem
UpperSemicontinuousAt.upperSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
{x : α}
(s : Set α)
(h : UpperSemicontinuousAt f x)
:
theorem
UpperSemicontinuousOn.upperSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
{x : α}
{s : Set α}
(h : UpperSemicontinuousOn f s)
(hx : x ∈ s)
:
theorem
UpperSemicontinuousOn.mono
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
{s : Set α}
{t : Set α}
(h : UpperSemicontinuousOn f s)
(hst : t ⊆ s)
:
theorem
upperSemicontinuousOn_univ_iff
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
:
UpperSemicontinuousOn f Set.univ ↔ UpperSemicontinuous f
theorem
UpperSemicontinuous.upperSemicontinuousAt
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
(h : UpperSemicontinuous f)
(x : α)
:
theorem
UpperSemicontinuous.upperSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
(h : UpperSemicontinuous f)
(s : Set α)
(x : α)
:
theorem
UpperSemicontinuous.upperSemicontinuousOn
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
(h : UpperSemicontinuous f)
(s : Set α)
:
Constants #
theorem
upperSemicontinuousWithinAt_const
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{x : α}
{s : Set α}
{z : β}
:
UpperSemicontinuousWithinAt (fun _x => z) s x
theorem
upperSemicontinuousAt_const
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{x : α}
{z : β}
:
UpperSemicontinuousAt (fun _x => z) x
theorem
upperSemicontinuousOn_const
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{s : Set α}
{z : β}
:
UpperSemicontinuousOn (fun _x => z) s
theorem
upperSemicontinuous_const
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{z : β}
:
UpperSemicontinuous fun _x => z
Indicators #
theorem
IsOpen.upperSemicontinuous_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{s : Set α}
{y : β}
[Zero β]
(hs : IsOpen s)
(hy : y ≤ 0)
:
UpperSemicontinuous (Set.indicator s fun _x => y)
theorem
IsOpen.upperSemicontinuousOn_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{s : Set α}
{t : Set α}
{y : β}
[Zero β]
(hs : IsOpen s)
(hy : y ≤ 0)
:
UpperSemicontinuousOn (Set.indicator s fun _x => y) t
theorem
IsOpen.upperSemicontinuousAt_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{x : α}
{s : Set α}
{y : β}
[Zero β]
(hs : IsOpen s)
(hy : y ≤ 0)
:
UpperSemicontinuousAt (Set.indicator s fun _x => y) x
theorem
IsOpen.upperSemicontinuousWithinAt_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{x : α}
{s : Set α}
{t : Set α}
{y : β}
[Zero β]
(hs : IsOpen s)
(hy : y ≤ 0)
:
UpperSemicontinuousWithinAt (Set.indicator s fun _x => y) t x
theorem
IsClosed.upperSemicontinuous_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{s : Set α}
{y : β}
[Zero β]
(hs : IsClosed s)
(hy : 0 ≤ y)
:
UpperSemicontinuous (Set.indicator s fun _x => y)
theorem
IsClosed.upperSemicontinuousOn_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{s : Set α}
{t : Set α}
{y : β}
[Zero β]
(hs : IsClosed s)
(hy : 0 ≤ y)
:
UpperSemicontinuousOn (Set.indicator s fun _x => y) t
theorem
IsClosed.upperSemicontinuousAt_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{x : α}
{s : Set α}
{y : β}
[Zero β]
(hs : IsClosed s)
(hy : 0 ≤ y)
:
UpperSemicontinuousAt (Set.indicator s fun _x => y) x
theorem
IsClosed.upperSemicontinuousWithinAt_indicator
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{x : α}
{s : Set α}
{t : Set α}
{y : β}
[Zero β]
(hs : IsClosed s)
(hy : 0 ≤ y)
:
UpperSemicontinuousWithinAt (Set.indicator s fun _x => y) t x
Relationship with continuity #
theorem
upperSemicontinuous_iff_isOpen_preimage
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
:
UpperSemicontinuous f ↔ ∀ (y : β), IsOpen (f ⁻¹' Set.Iio y)
theorem
UpperSemicontinuous.isOpen_preimage
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[Preorder β]
{f : α → β}
(hf : UpperSemicontinuous f)
(y : β)
:
theorem
upperSemicontinuous_iff_isClosed_preimage
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_3}
[LinearOrder γ]
{f : α → γ}
:
UpperSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Set.Ici y)
theorem
UpperSemicontinuous.isClosed_preimage
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_3}
[LinearOrder γ]
{f : α → γ}
(hf : UpperSemicontinuous f)
(y : γ)
:
theorem
ContinuousWithinAt.upperSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : ContinuousWithinAt f s x)
:
theorem
ContinuousAt.upperSemicontinuousAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : ContinuousAt f x)
:
theorem
ContinuousOn.upperSemicontinuousOn
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : ContinuousOn f s)
:
theorem
Continuous.upperSemicontinuous
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : Continuous f)
:
Composition #
theorem
ContinuousAt.comp_upperSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : ContinuousAt g (f x))
(hf : UpperSemicontinuousWithinAt f s x)
(gmon : Monotone g)
:
UpperSemicontinuousWithinAt (g ∘ f) s x
theorem
ContinuousAt.comp_upperSemicontinuousAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : ContinuousAt g (f x))
(hf : UpperSemicontinuousAt f x)
(gmon : Monotone g)
:
UpperSemicontinuousAt (g ∘ f) x
theorem
Continuous.comp_upperSemicontinuousOn
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : Continuous g)
(hf : UpperSemicontinuousOn f s)
(gmon : Monotone g)
:
UpperSemicontinuousOn (g ∘ f) s
theorem
Continuous.comp_upperSemicontinuous
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : Continuous g)
(hf : UpperSemicontinuous f)
(gmon : Monotone g)
:
UpperSemicontinuous (g ∘ f)
theorem
ContinuousAt.comp_upperSemicontinuousWithinAt_antitone
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : ContinuousAt g (f x))
(hf : UpperSemicontinuousWithinAt f s x)
(gmon : Antitone g)
:
LowerSemicontinuousWithinAt (g ∘ f) s x
theorem
ContinuousAt.comp_upperSemicontinuousAt_antitone
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : ContinuousAt g (f x))
(hf : UpperSemicontinuousAt f x)
(gmon : Antitone g)
:
LowerSemicontinuousAt (g ∘ f) x
theorem
Continuous.comp_upperSemicontinuousOn_antitone
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : Continuous g)
(hf : UpperSemicontinuousOn f s)
(gmon : Antitone g)
:
LowerSemicontinuousOn (g ∘ f) s
theorem
Continuous.comp_upperSemicontinuous_antitone
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_4}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : Continuous g)
(hf : UpperSemicontinuous f)
(gmon : Antitone g)
:
LowerSemicontinuous (g ∘ f)
Addition #
theorem
UpperSemicontinuousWithinAt.add'
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
{g : α → γ}
(hf : UpperSemicontinuousWithinAt f s x)
(hg : UpperSemicontinuousWithinAt g s x)
(hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x))
:
UpperSemicontinuousWithinAt (fun z => f z + g z) s x
The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to EReal. The unprimed version of
the lemma uses [ContinuousAdd].
theorem
UpperSemicontinuousAt.add'
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
{g : α → γ}
(hf : UpperSemicontinuousAt f x)
(hg : UpperSemicontinuousAt g x)
(hcont : ContinuousAt (fun p => p.fst + p.snd) (f x, g x))
:
UpperSemicontinuousAt (fun z => f z + g z) x
The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to EReal. The unprimed version of
the lemma uses [ContinuousAdd].
theorem
UpperSemicontinuousOn.add'
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
{g : α → γ}
(hf : UpperSemicontinuousOn f s)
(hg : UpperSemicontinuousOn g s)
(hcont : ∀ (x : α), x ∈ s → ContinuousAt (fun p => p.fst + p.snd) (f x, g x))
:
UpperSemicontinuousOn (fun z => f z + g z) s
The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to EReal. The unprimed version of
the lemma uses [ContinuousAdd].
theorem
UpperSemicontinuous.add'
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
{g : α → γ}
(hf : UpperSemicontinuous f)
(hg : UpperSemicontinuous g)
(hcont : ∀ (x : α), ContinuousAt (fun p => p.fst + p.snd) (f x, g x))
:
UpperSemicontinuous fun z => f z + g z
The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to EReal. The unprimed version of
the lemma uses [ContinuousAdd].
theorem
UpperSemicontinuousWithinAt.add
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : α → γ}
{g : α → γ}
(hf : UpperSemicontinuousWithinAt f s x)
(hg : UpperSemicontinuousWithinAt g s x)
:
UpperSemicontinuousWithinAt (fun z => f z + g z) s x
The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with
[ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to EReal.
theorem
UpperSemicontinuousAt.add
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : α → γ}
{g : α → γ}
(hf : UpperSemicontinuousAt f x)
(hg : UpperSemicontinuousAt g x)
:
UpperSemicontinuousAt (fun z => f z + g z) x
The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with
[ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to EReal.
theorem
UpperSemicontinuousOn.add
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : α → γ}
{g : α → γ}
(hf : UpperSemicontinuousOn f s)
(hg : UpperSemicontinuousOn g s)
:
UpperSemicontinuousOn (fun z => f z + g z) s
The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with
[ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to EReal.
theorem
UpperSemicontinuous.add
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : α → γ}
{g : α → γ}
(hf : UpperSemicontinuous f)
(hg : UpperSemicontinuous g)
:
UpperSemicontinuous fun z => f z + g z
The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with
[ContinuousAdd]. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to EReal.
theorem
upperSemicontinuousWithinAt_sum
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{ι : Type u_3}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ (i : ι), i ∈ a → UpperSemicontinuousWithinAt (f i) s x)
:
UpperSemicontinuousWithinAt (fun z => Finset.sum a fun i => f i z) s x
theorem
upperSemicontinuousAt_sum
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{ι : Type u_3}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ (i : ι), i ∈ a → UpperSemicontinuousAt (f i) x)
:
UpperSemicontinuousAt (fun z => Finset.sum a fun i => f i z) x
theorem
upperSemicontinuousOn_sum
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{ι : Type u_3}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ (i : ι), i ∈ a → UpperSemicontinuousOn (f i) s)
:
UpperSemicontinuousOn (fun z => Finset.sum a fun i => f i z) s
theorem
upperSemicontinuous_sum
{α : Type u_1}
[TopologicalSpace α]
{ι : Type u_3}
{γ : Type u_4}
[LinearOrderedAddCommMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ (i : ι), i ∈ a → UpperSemicontinuous (f i))
:
UpperSemicontinuous fun z => Finset.sum a fun i => f i z
Infimum #
theorem
upperSemicontinuousWithinAt_ciInf
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{ι : Sort u_3}
{δ' : Type u_5}
[ConditionallyCompleteLinearOrder δ']
{f : ι → α → δ'}
(bdd : ∀ᶠ (y : α) in nhdsWithin x s, BddBelow (Set.range fun i => f i y))
(h : ∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x)
:
UpperSemicontinuousWithinAt (fun x' => ⨅ (i : ι), f i x') s x
theorem
upperSemicontinuousWithinAt_iInf
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{f : ι → α → δ}
(h : ∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x)
:
UpperSemicontinuousWithinAt (fun x' => ⨅ (i : ι), f i x') s x
theorem
upperSemicontinuousWithinAt_biInf
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{p : ι → Prop}
{f : (i : ι) → p i → α → δ}
(h : ∀ (i : ι) (hi : p i), UpperSemicontinuousWithinAt (f i hi) s x)
:
UpperSemicontinuousWithinAt (fun x' => ⨅ (i : ι) (hi : p i), f i hi x') s x
theorem
upperSemicontinuousAt_ciInf
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{ι : Sort u_3}
{δ' : Type u_5}
[ConditionallyCompleteLinearOrder δ']
{f : ι → α → δ'}
(bdd : ∀ᶠ (y : α) in nhds x, BddBelow (Set.range fun i => f i y))
(h : ∀ (i : ι), UpperSemicontinuousAt (f i) x)
:
UpperSemicontinuousAt (fun x' => ⨅ (i : ι), f i x') x
theorem
upperSemicontinuousAt_iInf
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{f : ι → α → δ}
(h : ∀ (i : ι), UpperSemicontinuousAt (f i) x)
:
UpperSemicontinuousAt (fun x' => ⨅ (i : ι), f i x') x
theorem
upperSemicontinuousAt_biInf
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{p : ι → Prop}
{f : (i : ι) → p i → α → δ}
(h : ∀ (i : ι) (hi : p i), UpperSemicontinuousAt (f i hi) x)
:
UpperSemicontinuousAt (fun x' => ⨅ (i : ι) (hi : p i), f i hi x') x
theorem
upperSemicontinuousOn_ciInf
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{ι : Sort u_3}
{δ' : Type u_5}
[ConditionallyCompleteLinearOrder δ']
{f : ι → α → δ'}
(bdd : ∀ (x : α), x ∈ s → BddBelow (Set.range fun i => f i x))
(h : ∀ (i : ι), UpperSemicontinuousOn (f i) s)
:
UpperSemicontinuousOn (fun x' => ⨅ (i : ι), f i x') s
theorem
upperSemicontinuousOn_iInf
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{f : ι → α → δ}
(h : ∀ (i : ι), UpperSemicontinuousOn (f i) s)
:
UpperSemicontinuousOn (fun x' => ⨅ (i : ι), f i x') s
theorem
upperSemicontinuousOn_biInf
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{p : ι → Prop}
{f : (i : ι) → p i → α → δ}
(h : ∀ (i : ι) (hi : p i), UpperSemicontinuousOn (f i hi) s)
:
UpperSemicontinuousOn (fun x' => ⨅ (i : ι) (hi : p i), f i hi x') s
theorem
upperSemicontinuous_ciInf
{α : Type u_1}
[TopologicalSpace α]
{ι : Sort u_3}
{δ' : Type u_5}
[ConditionallyCompleteLinearOrder δ']
{f : ι → α → δ'}
(bdd : ∀ (x : α), BddBelow (Set.range fun i => f i x))
(h : ∀ (i : ι), UpperSemicontinuous (f i))
:
UpperSemicontinuous fun x' => ⨅ (i : ι), f i x'
theorem
upperSemicontinuous_iInf
{α : Type u_1}
[TopologicalSpace α]
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{f : ι → α → δ}
(h : ∀ (i : ι), UpperSemicontinuous (f i))
:
UpperSemicontinuous fun x' => ⨅ (i : ι), f i x'
theorem
upperSemicontinuous_biInf
{α : Type u_1}
[TopologicalSpace α]
{ι : Sort u_3}
{δ : Type u_4}
[CompleteLinearOrder δ]
{p : ι → Prop}
{f : (i : ι) → p i → α → δ}
(h : ∀ (i : ι) (hi : p i), UpperSemicontinuous (f i hi))
:
UpperSemicontinuous fun x' => ⨅ (i : ι) (hi : p i), f i hi x'
theorem
continuousWithinAt_iff_lower_upperSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
:
ContinuousWithinAt f s x ↔ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x
theorem
continuousAt_iff_lower_upperSemicontinuousAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
:
ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
theorem
continuousOn_iff_lower_upperSemicontinuousOn
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
:
ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
theorem
continuous_iff_lower_upperSemicontinuous
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_3}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
: