Lower and Upper Semicontinuity #
This file develops key properties of upper and lower semicontinuous functions.
Main definitions and results #
We have some equivalent definitions of lower- and upper-semicontinuity (under certain restrictions on the order on the codomain):
lowerSemicontinuous_iff_isOpen_preimagein a linear order;lowerSemicontinuous_iff_isClosed_preimagein a linear order;lowerSemicontinuousAt_iff_le_liminfin a complete linear order;lowerSemicontinuous_iff_isClosed_epigraphin a linear order with the order topology.
We also prove:
indicator s (fun _ ↦ y)is lower semicontinuous whensis open and0 ≤ y, or whensis closed andy ≤ 0;- continuous functions are lower semicontinuous;
- left 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.
References #
- lower and upper semicontinuity correspond to
r := (f · > ·)andr := (f · < ·); - lower and upper hemicontinuity correspond to
r := (fun x s ↦ IsOpen s ∧ ((f x) ∩ s).Nonempty)andr := (fun x s ↦ s ∈ 𝓝ˢ (f x)), respectively.
lower bounds #
theorem
LowerSemicontinuousOn.exists_isMinOn
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{f : α → β}
[LinearOrder β]
{s : Set α}
(ne_s : s.Nonempty)
(hs : IsCompact s)
(hf : LowerSemicontinuousOn f s)
:
∃ a ∈ s, IsMinOn f s a
A lower semicontinuous function attains its lower bound on a nonempty compact set.
theorem
LowerSemicontinuousOn.bddBelow_of_isCompact
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{f : α → β}
[LinearOrder β]
[Nonempty β]
{s : Set α}
(hs : IsCompact s)
(hf : LowerSemicontinuousOn f s)
:
A lower semicontinuous function is bounded below on a compact set.
Indicators #
theorem
IsOpen.lowerSemicontinuous_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s : Set α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsOpen s)
(hy : 0 ≤ y)
:
LowerSemicontinuous (s.indicator fun (_x : α) => y)
theorem
IsOpen.lowerSemicontinuousOn_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s t : Set α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsOpen s)
(hy : 0 ≤ y)
:
LowerSemicontinuousOn (s.indicator fun (_x : α) => y) t
theorem
IsOpen.lowerSemicontinuousAt_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s : Set α}
{x : α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsOpen s)
(hy : 0 ≤ y)
:
LowerSemicontinuousAt (s.indicator fun (_x : α) => y) x
theorem
IsOpen.lowerSemicontinuousWithinAt_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s t : Set α}
{x : α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsOpen s)
(hy : 0 ≤ y)
:
LowerSemicontinuousWithinAt (s.indicator fun (_x : α) => y) t x
theorem
IsClosed.lowerSemicontinuous_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s : Set α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsClosed s)
(hy : y ≤ 0)
:
LowerSemicontinuous (s.indicator fun (_x : α) => y)
theorem
IsClosed.lowerSemicontinuousOn_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s t : Set α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsClosed s)
(hy : y ≤ 0)
:
LowerSemicontinuousOn (s.indicator fun (_x : α) => y) t
theorem
IsClosed.lowerSemicontinuousAt_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s : Set α}
{x : α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsClosed s)
(hy : y ≤ 0)
:
LowerSemicontinuousAt (s.indicator fun (_x : α) => y) x
theorem
IsClosed.lowerSemicontinuousWithinAt_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s t : Set α}
{x : α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsClosed s)
(hy : y ≤ 0)
:
LowerSemicontinuousWithinAt (s.indicator fun (_x : α) => y) t x
Relationship with continuity #
theorem
lowerSemicontinuous_iff_isOpen_preimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{f : α → β}
[Preorder β]
:
theorem
LowerSemicontinuous.isOpen_preimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{f : α → β}
[Preorder β]
(hf : LowerSemicontinuous f)
(y : β)
:
theorem
lowerSemicontinuous_iff_isClosed_preimage
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrder γ]
{f : α → γ}
:
theorem
LowerSemicontinuous.isClosed_preimage
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrder γ]
{f : α → γ}
(hf : LowerSemicontinuous f)
(y : γ)
:
theorem
lowerSemicontinuousOn_iff_preimage_Iic
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrder γ]
{f : α → γ}
:
theorem
ContinuousWithinAt.lowerSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{x : α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : ContinuousWithinAt f s x)
:
theorem
ContinuousAt.lowerSemicontinuousAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : ContinuousAt f x)
:
theorem
ContinuousOn.lowerSemicontinuousOn
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : ContinuousOn f s)
:
theorem
Continuous.lowerSemicontinuous
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : Continuous f)
:
Equivalent definitions #
theorem
lowerSemicontinuousWithinAt_iff_le_liminf
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{x : α}
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
theorem
LowerSemicontinuousWithinAt.le_liminf
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{x : α}
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
LowerSemicontinuousWithinAt f s x → f x ≤ Filter.liminf f (nhdsWithin x s)
Alias of the forward direction of lowerSemicontinuousWithinAt_iff_le_liminf.
theorem
lowerSemicontinuousAt_iff_le_liminf
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
theorem
LowerSemicontinuousAt.le_liminf
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
LowerSemicontinuousAt f x → f x ≤ Filter.liminf f (nhds x)
Alias of the forward direction of lowerSemicontinuousAt_iff_le_liminf.
theorem
lowerSemicontinuous_iff_le_liminf
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
theorem
LowerSemicontinuous.le_liminf
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
LowerSemicontinuous f → ∀ (x : α), f x ≤ Filter.liminf f (nhds x)
Alias of the forward direction of lowerSemicontinuous_iff_le_liminf.
theorem
lowerSemicontinuousOn_iff_le_liminf
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
theorem
LowerSemicontinuousOn.le_liminf
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
LowerSemicontinuousOn f s → ∀ x ∈ s, f x ≤ Filter.liminf f (nhdsWithin x s)
Alias of the forward direction of lowerSemicontinuousOn_iff_le_liminf.
theorem
LowerSemicontinuousOn.isCompact_inter_preimage_Iic
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrder γ]
{f : α → γ}
(hfs : LowerSemicontinuousOn f s)
(ks : IsCompact s)
(c : γ)
:
The sublevel sets of a lower semicontinuous function on a compact set are compact.
theorem
LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrder γ]
{ι : Type u_5}
{f : ι → α → γ}
(ks : IsCompact s)
{I : Set ι}
{c : γ}
(hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s)
:
An intersection of sublevel sets of a lower semicontinuous function on a compact set is empty if and only if a finite sub-intersection is already empty.
theorem
lowerSemicontinuousOn_iff_isClosed_epigraph
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[ClosedIciTopology γ]
{f : α → γ}
{s : Set α}
(hs : IsClosed s)
:
theorem
lowerSemicontinuous_iff_isClosed_epigraph
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[ClosedIciTopology γ]
{f : α → γ}
:
theorem
LowerSemicontinuous.isClosed_epigraph
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[ClosedIciTopology γ]
{f : α → γ}
:
Alias of the forward direction of lowerSemicontinuous_iff_isClosed_epigraph.
Composition #
theorem
ContinuousAt.comp_lowerSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{x : α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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 α]
{s : Set α}
{x : α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : Continuous g)
(hf : LowerSemicontinuous f)
(gmon : Antitone g)
:
UpperSemicontinuous (g ∘ f)
@[deprecated LowerSemicontinuousAt.comp (since := "2025-12-06")]
theorem
LowerSemicontinuousAt.comp_continuousAt
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace γ]
[Preorder β]
{f : α → β}
{g : γ → α}
{x : γ}
(hf : LowerSemicontinuousAt f (g x))
(hg : ContinuousAt g x)
:
LowerSemicontinuousAt (f ∘ g) x
Alias of LowerSemicontinuousAt.comp.
@[deprecated LowerSemicontinuousAt.comp (since := "2025-12-06")]
theorem
LowerSemicontinuousAt.comp_continuousAt_of_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace γ]
[Preorder β]
{f : α → β}
{g : γ → α}
{x : γ}
(hf : LowerSemicontinuousAt f (g x))
(hg : ContinuousAt g x)
:
LowerSemicontinuousAt (f ∘ g) x
Alias of LowerSemicontinuousAt.comp.
@[deprecated LowerSemicontinuous.comp (since := "2025-12-06")]
theorem
LowerSemicontinuous.comp_continuous
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace γ]
[Preorder β]
{f : α → β}
{g : γ → α}
(hf : LowerSemicontinuous f)
(hg : Continuous g)
:
LowerSemicontinuous (f ∘ g)
Alias of LowerSemicontinuous.comp.
Addition #
theorem
LowerSemicontinuousWithinAt.add'
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{x : α}
{γ : Type u_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f g : α → γ}
(hf : LowerSemicontinuousWithinAt f s x)
(hg : LowerSemicontinuousWithinAt g s x)
(hcont : ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (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_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f g : α → γ}
(hf : LowerSemicontinuousAt f x)
(hg : LowerSemicontinuousAt g x)
(hcont : ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (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_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f g : α → γ}
(hf : LowerSemicontinuousOn f s)
(hg : LowerSemicontinuousOn g s)
(hcont : ∀ x ∈ s, ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (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_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f g : α → γ}
(hf : LowerSemicontinuous f)
(hg : LowerSemicontinuous g)
(hcont : ∀ (x : α), ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (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 α]
{s : Set α}
{x : α}
{γ : Type u_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[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_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[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_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[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_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[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 α]
{s : Set α}
{x : α}
{ι : Type u_4}
{γ : Type u_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) s x)
:
LowerSemicontinuousWithinAt (fun (z : α) => ∑ i ∈ a, f i z) s x
theorem
lowerSemicontinuousAt_sum
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{ι : Type u_4}
{γ : Type u_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ i ∈ a, LowerSemicontinuousAt (f i) x)
:
LowerSemicontinuousAt (fun (z : α) => ∑ i ∈ a, f i z) x
theorem
lowerSemicontinuousOn_sum
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{ι : Type u_4}
{γ : Type u_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ i ∈ a, LowerSemicontinuousOn (f i) s)
:
LowerSemicontinuousOn (fun (z : α) => ∑ i ∈ a, f i z) s
theorem
lowerSemicontinuous_sum
{α : Type u_1}
[TopologicalSpace α]
{ι : Type u_4}
{γ : Type u_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ i ∈ a, LowerSemicontinuous (f i))
:
LowerSemicontinuous fun (z : α) => ∑ i ∈ a, f i z
Supremum #
theorem
LowerSemicontinuousWithinAt.sup
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{s : Set α}
{a : α}
(hf : LowerSemicontinuousWithinAt f s a)
(hg : LowerSemicontinuousWithinAt g s a)
:
LowerSemicontinuousWithinAt (fun (x : α) => max (f x) (g x)) s a
theorem
LowerSemicontinuousAt.sup
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{a : α}
(hf : LowerSemicontinuousAt f a)
(hg : LowerSemicontinuousAt g a)
:
LowerSemicontinuousAt (fun (x : α) => max (f x) (g x)) a
theorem
LowerSemicontinuousOn.sup
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{s : Set α}
(hf : LowerSemicontinuousOn f s)
(hg : LowerSemicontinuousOn g s)
:
LowerSemicontinuousOn (fun (x : α) => max (f x) (g x)) s
theorem
LowerSemicontinuous.sup
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
(hf : LowerSemicontinuous f)
(hg : LowerSemicontinuous g)
:
LowerSemicontinuous fun (x : α) => max (f x) (g x)
theorem
LowerSemicontinuousWithinAt.inf
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{s : Set α}
{a : α}
(hf : LowerSemicontinuousWithinAt f s a)
(hg : LowerSemicontinuousWithinAt g s a)
:
LowerSemicontinuousWithinAt (fun (x : α) => min (f x) (g x)) s a
theorem
LowerSemicontinuousAt.inf
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{a : α}
(hf : LowerSemicontinuousAt f a)
(hg : LowerSemicontinuousAt g a)
:
LowerSemicontinuousAt (fun (x : α) => min (f x) (g x)) a
theorem
LowerSemicontinuousOn.inf
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{s : Set α}
(hf : LowerSemicontinuousOn f s)
(hg : LowerSemicontinuousOn g s)
:
LowerSemicontinuousOn (fun (x : α) => min (f x) (g x)) s
theorem
LowerSemicontinuous.inf
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
(hf : LowerSemicontinuous f)
(hg : LowerSemicontinuous g)
:
LowerSemicontinuous fun (x : α) => min (f x) (g x)
theorem
lowerSemicontinuousWithinAt_ciSup
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{x : α}
{ι : Sort u_4}
{δ' : Type u_6}
[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 α]
{s : Set α}
{x : α}
{ι : Sort u_4}
{δ : Type u_5}
[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 α]
{s : Set α}
{x : α}
{ι : Sort u_4}
{δ : Type u_5}
[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_4}
{δ' : Type u_6}
[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_4}
{δ : Type u_5}
[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_4}
{δ : Type u_5}
[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_4}
{δ' : Type u_6}
[ConditionallyCompleteLinearOrder δ']
{f : ι → α → δ'}
(bdd : ∀ 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_4}
{δ : Type u_5}
[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_4}
{δ : Type u_5}
[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_4}
{δ' : Type u_6}
[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_4}
{δ : Type u_5}
[CompleteLinearOrder δ]
{f : ι → α → δ}
(h : ∀ (i : ι), LowerSemicontinuous (f i))
:
LowerSemicontinuous fun (x' : α) => ⨆ (i : ι), f i x'
theorem
lowerSemicontinuous_biSup
{α : Type u_1}
[TopologicalSpace α]
{ι : Sort u_4}
{δ : Type u_5}
[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 α]
{s : Set α}
{x : α}
{ι : Type u_4}
{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_4}
{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_4}
{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_4}
{f : ι → α → ENNReal}
(h : ∀ (i : ι), LowerSemicontinuous (f i))
:
LowerSemicontinuous fun (x' : α) => ∑' (i : ι), f i x'
Upper semicontinuous functions #
upper bounds #
theorem
UpperSemicontinuousOn.exists_isMaxOn
{α : Type u_4}
[TopologicalSpace α]
{β : Type u_5}
[LinearOrder β]
{f : α → β}
{s : Set α}
(ne_s : s.Nonempty)
(hs : IsCompact s)
(hf : UpperSemicontinuousOn f s)
:
∃ a ∈ s, IsMaxOn f s a
An upper semicontinuous function attains its upper bound on a nonempty compact set.
theorem
UpperSemicontinuousOn.bddAbove_of_isCompact
{α : Type u_4}
[TopologicalSpace α]
{β : Type u_5}
[LinearOrder β]
{f : α → β}
[Nonempty β]
{s : Set α}
(hs : IsCompact s)
(hf : UpperSemicontinuousOn f s)
:
An upper semicontinuous function is bounded above on a compact set.
Indicators #
theorem
IsOpen.upperSemicontinuous_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s : Set α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsOpen s)
(hy : y ≤ 0)
:
UpperSemicontinuous (s.indicator fun (_x : α) => y)
theorem
IsOpen.upperSemicontinuousOn_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s t : Set α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsOpen s)
(hy : y ≤ 0)
:
UpperSemicontinuousOn (s.indicator fun (_x : α) => y) t
theorem
IsOpen.upperSemicontinuousAt_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s : Set α}
{x : α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsOpen s)
(hy : y ≤ 0)
:
UpperSemicontinuousAt (s.indicator fun (_x : α) => y) x
theorem
IsOpen.upperSemicontinuousWithinAt_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s t : Set α}
{x : α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsOpen s)
(hy : y ≤ 0)
:
UpperSemicontinuousWithinAt (s.indicator fun (_x : α) => y) t x
theorem
IsClosed.upperSemicontinuous_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s : Set α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsClosed s)
(hy : 0 ≤ y)
:
UpperSemicontinuous (s.indicator fun (_x : α) => y)
theorem
IsClosed.upperSemicontinuousOn_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s t : Set α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsClosed s)
(hy : 0 ≤ y)
:
UpperSemicontinuousOn (s.indicator fun (_x : α) => y) t
theorem
IsClosed.upperSemicontinuousAt_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s : Set α}
{x : α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsClosed s)
(hy : 0 ≤ y)
:
UpperSemicontinuousAt (s.indicator fun (_x : α) => y) x
theorem
IsClosed.upperSemicontinuousWithinAt_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{s t : Set α}
{x : α}
{y : β}
[Zero β]
[Preorder β]
(hs : IsClosed s)
(hy : 0 ≤ y)
:
UpperSemicontinuousWithinAt (s.indicator fun (_x : α) => y) t x
Relationship with continuity #
theorem
upperSemicontinuous_iff_isOpen_preimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{f : α → β}
[Preorder β]
:
theorem
UpperSemicontinuous.isOpen_preimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
{f : α → β}
[Preorder β]
(hf : UpperSemicontinuous f)
(y : β)
:
theorem
upperSemicontinuous_iff_isClosed_preimage
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrder γ]
{f : α → γ}
:
theorem
UpperSemicontinuous.isClosed_preimage
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrder γ]
{f : α → γ}
(hf : UpperSemicontinuous f)
(y : γ)
:
theorem
ContinuousWithinAt.upperSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{x : α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : ContinuousWithinAt f s x)
:
theorem
ContinuousAt.upperSemicontinuousAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : ContinuousAt f x)
:
theorem
ContinuousOn.upperSemicontinuousOn
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : ContinuousOn f s)
:
theorem
Continuous.upperSemicontinuous
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
(h : Continuous f)
:
Equivalent definitions #
theorem
upperSemicontinuousWithinAt_iff_limsup_le
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{x : α}
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
theorem
UpperSemicontinuousWithinAt.limsup_le
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{x : α}
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
UpperSemicontinuousWithinAt f s x → Filter.limsup f (nhdsWithin x s) ≤ f x
Alias of the forward direction of upperSemicontinuousWithinAt_iff_limsup_le.
theorem
upperSemicontinuousAt_iff_limsup_le
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
theorem
UpperSemicontinuousAt.limsup_le
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
UpperSemicontinuousAt f x → Filter.limsup f (nhds x) ≤ f x
Alias of the forward direction of upperSemicontinuousAt_iff_limsup_le.
theorem
upperSemicontinuous_iff_limsup_le
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
theorem
UpperSemicontinuous.limsup_le
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
UpperSemicontinuous f → ∀ (x : α), Filter.limsup f (nhds x) ≤ f x
Alias of the forward direction of upperSemicontinuous_iff_limsup_le.
theorem
upperSemicontinuousOn_iff_limsup_le
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
theorem
UpperSemicontinuousOn.limsup_le
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[CompleteLinearOrder γ]
{f : α → γ}
:
UpperSemicontinuousOn f s → ∀ x ∈ s, Filter.limsup f (nhdsWithin x s) ≤ f x
Alias of the forward direction of upperSemicontinuousOn_iff_limsup_le.
theorem
UpperSemicontinuousOn.isCompact_inter_preimage_Ici
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrder γ]
{f : α → γ}
(hfs : UpperSemicontinuousOn f s)
(ks : IsCompact s)
(c : γ)
:
The overlevel sets of an upper semicontinuous function on a compact set are compact.
theorem
UpperSemicontinuousOn.inter_biInter_preimage_Ici_eq_empty_iff_exists_finset
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrder γ]
{ι : Type u_5}
{f : ι → α → γ}
(ks : IsCompact s)
{I : Set ι}
{c : γ}
(hfi : ∀ i ∈ I, UpperSemicontinuousOn (f i) s)
:
An intersection of overlevel sets of a lower semicontinuous function on a compact set is empty if and only if a finite sub-intersection is already empty.
theorem
upperSemicontinuousOn_iff_isClosed_hypograph
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[ClosedIicTopology γ]
{f : α → γ}
(hs : IsClosed s)
:
theorem
upperSemicontinuous_iff_IsClosed_hypograph
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[ClosedIicTopology γ]
{f : α → γ}
:
theorem
UpperSemicontinuous.IsClosed_hypograph
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[ClosedIicTopology γ]
{f : α → γ}
:
Alias of the forward direction of upperSemicontinuous_iff_IsClosed_hypograph.
Composition #
theorem
upperSemicontinuousOn_iff_preimage_Iio
{α : Type u_4}
[TopologicalSpace α]
{β : Type u_5}
[LinearOrder β]
{f : α → β}
{s : Set α}
:
theorem
upperSemicontinuousOn_iff_preimage_Ici
{α : Type u_4}
[TopologicalSpace α]
{β : Type u_5}
[LinearOrder β]
{f : α → β}
{s : Set α}
:
theorem
ContinuousAt.comp_upperSemicontinuousWithinAt
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{x : α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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 α]
{s : Set α}
{x : α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[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_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{δ : Type u_5}
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
{g : γ → δ}
{f : α → γ}
(hg : Continuous g)
(hf : UpperSemicontinuous f)
(gmon : Antitone g)
:
LowerSemicontinuous (g ∘ f)
@[deprecated UpperSemicontinuousAt.comp (since := "2025-12-06")]
theorem
UpperSemicontinuousAt.comp_continuousAt
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace γ]
[Preorder β]
{f : α → β}
{g : γ → α}
{c : γ}
(hf : UpperSemicontinuousAt f (g c))
(hg : ContinuousAt g c)
:
UpperSemicontinuousAt (f ∘ g) c
Alias of UpperSemicontinuousAt.comp.
@[deprecated UpperSemicontinuousAt.comp (since := "2025-12-06")]
theorem
UpperSemicontinuousAt.comp_continuousAt_of_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace γ]
[Preorder β]
{f : α → β}
{g : γ → α}
{c : γ}
(hf : UpperSemicontinuousAt f (g c))
(hg : ContinuousAt g c)
:
UpperSemicontinuousAt (f ∘ g) c
Alias of UpperSemicontinuousAt.comp.
@[deprecated UpperSemicontinuous.comp (since := "2025-12-06")]
theorem
UpperSemicontinuous.comp_continuous
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace γ]
[Preorder β]
{f : α → β}
{g : γ → α}
(hf : UpperSemicontinuous f)
(hg : Continuous g)
:
UpperSemicontinuous (f ∘ g)
Alias of UpperSemicontinuous.comp.
Addition #
theorem
UpperSemicontinuousWithinAt.add'
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{x : α}
{γ : Type u_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f g : α → γ}
(hf : UpperSemicontinuousWithinAt f s x)
(hg : UpperSemicontinuousWithinAt g s x)
(hcont : ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (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_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f g : α → γ}
(hf : UpperSemicontinuousAt f x)
(hg : UpperSemicontinuousAt g x)
(hcont : ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (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_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f g : α → γ}
(hf : UpperSemicontinuousOn f s)
(hg : UpperSemicontinuousOn g s)
(hcont : ∀ x ∈ s, ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (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_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f g : α → γ}
(hf : UpperSemicontinuous f)
(hg : UpperSemicontinuous g)
(hcont : ∀ (x : α), ContinuousAt (fun (p : γ × γ) => p.1 + p.2) (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 α]
{s : Set α}
{x : α}
{γ : Type u_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[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_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[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_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[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_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[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 α]
{s : Set α}
{x : α}
{ι : Type u_4}
{γ : Type u_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) s x)
:
UpperSemicontinuousWithinAt (fun (z : α) => ∑ i ∈ a, f i z) s x
theorem
upperSemicontinuousAt_sum
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{ι : Type u_4}
{γ : Type u_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ i ∈ a, UpperSemicontinuousAt (f i) x)
:
UpperSemicontinuousAt (fun (z : α) => ∑ i ∈ a, f i z) x
theorem
upperSemicontinuousOn_sum
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{ι : Type u_4}
{γ : Type u_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ i ∈ a, UpperSemicontinuousOn (f i) s)
:
UpperSemicontinuousOn (fun (z : α) => ∑ i ∈ a, f i z) s
theorem
upperSemicontinuous_sum
{α : Type u_1}
[TopologicalSpace α]
{ι : Type u_4}
{γ : Type u_5}
[AddCommMonoid γ]
[LinearOrder γ]
[IsOrderedAddMonoid γ]
[TopologicalSpace γ]
[OrderTopology γ]
[ContinuousAdd γ]
{f : ι → α → γ}
{a : Finset ι}
(ha : ∀ i ∈ a, UpperSemicontinuous (f i))
:
UpperSemicontinuous fun (z : α) => ∑ i ∈ a, f i z
Infimum #
theorem
UpperSemicontinuousWithinAt.inf
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{s : Set α}
{a : α}
(hf : UpperSemicontinuousWithinAt f s a)
(hg : UpperSemicontinuousWithinAt g s a)
:
UpperSemicontinuousWithinAt (fun (x : α) => min (f x) (g x)) s a
theorem
UpperSemicontinuousAt.inf
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{a : α}
(hf : UpperSemicontinuousAt f a)
(hg : UpperSemicontinuousAt g a)
:
UpperSemicontinuousAt (fun (x : α) => min (f x) (g x)) a
theorem
UpperSemicontinuousOn.inf
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{s : Set α}
(hf : UpperSemicontinuousOn f s)
(hg : UpperSemicontinuousOn g s)
:
UpperSemicontinuousOn (fun (x : α) => min (f x) (g x)) s
theorem
UpperSemicontinuous.inf
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
(hf : UpperSemicontinuous f)
(hg : UpperSemicontinuous g)
:
UpperSemicontinuous fun (x : α) => min (f x) (g x)
theorem
UpperSemicontinuousWithinAt.sup
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{s : Set α}
{a : α}
(hf : UpperSemicontinuousWithinAt f s a)
(hg : UpperSemicontinuousWithinAt g s a)
:
UpperSemicontinuousWithinAt (fun (x : α) => max (f x) (g x)) s a
theorem
UpperSemicontinuousAt.sup
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{a : α}
(hf : UpperSemicontinuousAt f a)
(hg : UpperSemicontinuousAt g a)
:
UpperSemicontinuousAt (fun (x : α) => max (f x) (g x)) a
theorem
UpperSemicontinuousOn.sup
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{s : Set α}
(hf : UpperSemicontinuousOn f s)
(hg : UpperSemicontinuousOn g s)
:
UpperSemicontinuousOn (fun (x : α) => max (f x) (g x)) s
theorem
UpperSemicontinuous.sup
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
(hf : UpperSemicontinuous f)
(hg : UpperSemicontinuous g)
:
UpperSemicontinuous fun (x : α) => max (f x) (g x)
theorem
upperSemicontinuousWithinAt_ciInf
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{x : α}
{ι : Sort u_4}
{δ' : Type u_6}
[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 α]
{s : Set α}
{x : α}
{ι : Sort u_4}
{δ : Type u_5}
[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 α]
{s : Set α}
{x : α}
{ι : Sort u_4}
{δ : Type u_5}
[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_4}
{δ' : Type u_6}
[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_4}
{δ : Type u_5}
[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_4}
{δ : Type u_5}
[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_4}
{δ' : Type u_6}
[ConditionallyCompleteLinearOrder δ']
{f : ι → α → δ'}
(bdd : ∀ 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_4}
{δ : Type u_5}
[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_4}
{δ : Type u_5}
[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_4}
{δ' : Type u_6}
[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_4}
{δ : Type u_5}
[CompleteLinearOrder δ]
{f : ι → α → δ}
(h : ∀ (i : ι), UpperSemicontinuous (f i))
:
UpperSemicontinuous fun (x' : α) => ⨅ (i : ι), f i x'
theorem
upperSemicontinuous_biInf
{α : Type u_1}
[TopologicalSpace α]
{ι : Sort u_4}
{δ : Type u_5}
[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 α]
{s : Set α}
{x : α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
:
theorem
continuousAt_iff_lower_upperSemicontinuousAt
{α : Type u_1}
[TopologicalSpace α]
{x : α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
:
theorem
continuousOn_iff_lower_upperSemicontinuousOn
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
:
theorem
continuous_iff_lower_upperSemicontinuous
{α : Type u_1}
[TopologicalSpace α]
{γ : Type u_4}
[LinearOrder γ]
[TopologicalSpace γ]
[OrderTopology γ]
{f : α → γ}
: