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 x
• LowerSemicontinuousAt f x
• LowerSemicontinuousOn f s
• LowerSemicontinuous f

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

• constant functions are lower semicontinuous;
• indicator s (fun _ ↦ y) is lower semicontinuous when s is open and 0 ≤ y, or when s is closed and y ≤ 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;
• right composition with continuous functions preserves lower and upper semicontinuity;
• 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.

We have some equivalent definitions of lower- and upper-semicontinuity (under certain restrictions on the order on the codomain):

• lowerSemicontinuous_iff_isOpen_preimage in a linear order;
• lowerSemicontinuous_iff_isClosed_preimage in a linear order;
• lowerSemicontinuousAt_iff_le_liminf in a dense complete linear order;
• lowerSemicontinuous_iff_isClosed_epigraph in a dense complete linear order with the order topology.

Implementation details

All the nontrivial results for upper semicontinuous functions are deduced from the corresponding ones for lower semicontinuous functions using OrderDual.

References

• https://en.wikipedia.org/wiki/Closed_convex_function
• https://en.wikipedia.org/wiki/Semi-continuity

Main definitions

def LowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (s : Set α) (x : α) : Prop

A real function f is lower semicontinuous at x within a set s if, for any ε > 0, for all x' close enough to x in s, then f x' is at least f x - ε. We formulate this in a general preordered space, using an arbitrary y < f x instead of f x - ε.

Equations

• LowerSemicontinuousWithinAt f s x = ∀ y < f x, ∀ᶠ (x' : α) in nhdsWithin x s, y < f x'

def LowerSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (s : Set α) : Prop

A real function f is lower semicontinuous on a set s if, for any ε > 0, for any x ∈ s, for all x' close enough to x in s, then f x' is at least f x - ε. We formulate this in a general preordered space, using an arbitrary y < f x instead of f x - ε.

Equations

• LowerSemicontinuousOn f s = ∀ x ∈ s, LowerSemicontinuousWithinAt f s x

def LowerSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (x : α) : Prop

A real function f is lower semicontinuous at x if, for any ε > 0, for all x' close enough to x, then f x' is at least f x - ε. We formulate this in a general preordered space, using an arbitrary y < f x instead of f x - ε.

Equations

• LowerSemicontinuousAt f x = ∀ y < f x, ∀ᶠ (x' : α) in nhds x, y < f x'

def LowerSemicontinuous {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) : Prop

A real function f is lower semicontinuous if, for any ε > 0, for any x, for all x' close enough to x, then f x' is at least f x - ε. We formulate this in a general preordered space, using an arbitrary y < f x instead of f x - ε.

Equations

• LowerSemicontinuous f = ∀ (x : α), LowerSemicontinuousAt f x

def UpperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (s : Set α) (x : α) : Prop

A real function f is upper semicontinuous at x within a set s if, for any ε > 0, for all x' close enough to x in s, then f x' is at most f x + ε. We formulate this in a general preordered space, using an arbitrary y > f x instead of f x + ε.

Equations

• UpperSemicontinuousWithinAt f s x = ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhdsWithin x s, f x' < y

def UpperSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (s : Set α) : Prop

A real function f is upper semicontinuous on a set s if, for any ε > 0, for any x ∈ s, for all x' close enough to x in s, then f x' is at most f x + ε. We formulate this in a general preordered space, using an arbitrary y > f x instead of f x + ε.

Equations

• UpperSemicontinuousOn f s = ∀ x ∈ s, UpperSemicontinuousWithinAt f s x

def UpperSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (x : α) : Prop

A real function f is upper semicontinuous at x if, for any ε > 0, for all x' close enough to x, then f x' is at most f x + ε. We formulate this in a general preordered space, using an arbitrary y > f x instead of f x + ε.

Equations

• UpperSemicontinuousAt f x = ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhds x, f x' < y

def UpperSemicontinuous {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) : Prop

A real function f is upper semicontinuous if, for any ε > 0, for any x, for all x' close enough to x, then f x' is at most f x + ε. We formulate this in a general preordered space, using an arbitrary y > f x instead of f x + ε.

Equations

• UpperSemicontinuous f = ∀ (x : α), UpperSemicontinuousAt f x

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) : LowerSemicontinuousWithinAt f t x

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) : LowerSemicontinuousWithinAt f s x

theorem LowerSemicontinuousOn.lowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {x : α} {s : Set α} (h : LowerSemicontinuousOn f s) (hx : x ∈ s) : LowerSemicontinuousWithinAt f s x

theorem LowerSemicontinuousOn.mono {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {s : Set α} {t : Set α} (h : LowerSemicontinuousOn f s) (hst : t ⊆ s) : LowerSemicontinuousOn f t

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 : α) : LowerSemicontinuousAt f x

theorem LowerSemicontinuous.lowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} (h : LowerSemicontinuous f) (s : Set α) (x : α) : LowerSemicontinuousWithinAt f s x

theorem LowerSemicontinuous.lowerSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} (h : LowerSemicontinuous f) (s : Set α) : LowerSemicontinuousOn f s

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 (s.indicator 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 (s.indicator 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 (s.indicator 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 (s.indicator 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 (s.indicator 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 (s.indicator 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 (s.indicator 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 (s.indicator 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 : β) : IsOpen (f ⁻¹' Set.Ioi 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 : γ) : IsClosed (f ⁻¹' Set.Iic y)

theorem ContinuousWithinAt.lowerSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : ContinuousWithinAt f s x) : LowerSemicontinuousWithinAt f s x

theorem ContinuousAt.lowerSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : ContinuousAt f x) : LowerSemicontinuousAt f x

theorem ContinuousOn.lowerSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : ContinuousOn f s) : LowerSemicontinuousOn f s

theorem Continuous.lowerSemicontinuous {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : Continuous f) : LowerSemicontinuous f

Equivalent definitions

theorem lowerSemicontinuousWithinAt_iff_le_liminf {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : α → γ} : LowerSemicontinuousWithinAt f s x ↔ f x ≤ Filter.liminf f (nhdsWithin x s)

theorem LowerSemicontinuousWithinAt.le_liminf {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {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_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : α → γ} : LowerSemicontinuousAt f x ↔ f x ≤ Filter.liminf f (nhds x)

theorem LowerSemicontinuousAt.le_liminf {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {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_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : α → γ} : LowerSemicontinuous f ↔ ∀ (x : α), f x ≤ Filter.liminf f (nhds x)

theorem LowerSemicontinuous.le_liminf {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {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_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : α → γ} : LowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ Filter.liminf f (nhdsWithin x s)

theorem LowerSemicontinuousOn.le_liminf {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {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 lowerSemicontinuous_iff_isClosed_epigraph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} : LowerSemicontinuous f ↔ IsClosed {p : α × γ | f p.1 ≤ p.2}

@[deprecated lowerSemicontinuous_iff_isClosed_epigraph]

theorem lowerSemicontinuous_iff_IsClosed_epigraph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} : LowerSemicontinuous f ↔ IsClosed {p : α × γ | f p.1 ≤ p.2}

Alias of lowerSemicontinuous_iff_isClosed_epigraph.

theorem LowerSemicontinuous.isClosed_epigraph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} : LowerSemicontinuous f → IsClosed {p : α × γ | f p.1 ≤ p.2}

Alias of the forward direction of lowerSemicontinuous_iff_isClosed_epigraph.

@[deprecated LowerSemicontinuous.isClosed_epigraph]

theorem LowerSemicontinuous.IsClosed_epigraph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} : LowerSemicontinuous f → IsClosed {p : α × γ | f p.1 ≤ p.2}

Alias of the forward direction of lowerSemicontinuous_iff_isClosed_epigraph.

---

Alias of the forward direction of lowerSemicontinuous_iff_isClosed_epigraph.

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)

theorem LowerSemicontinuousAt.comp_continuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : α → β} {g : ι → α} {x : ι} (hf : LowerSemicontinuousAt f (g x)) (hg : ContinuousAt g x) : LowerSemicontinuousAt (fun (x : ι) => f (g x)) x

theorem LowerSemicontinuousAt.comp_continuousAt_of_eq {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : α → β} {g : ι → α} {y : α} {x : ι} (hf : LowerSemicontinuousAt f y) (hg : ContinuousAt g x) (hy : g x = y) : LowerSemicontinuousAt (fun (x : ι) => f (g x)) x

theorem LowerSemicontinuous.comp_continuous {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : α → β} {g : ι → α} (hf : LowerSemicontinuous f) (hg : Continuous g) : LowerSemicontinuous fun (x : ι) => f (g x)

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.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_4} [LinearOrderedAddCommMonoid γ] [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_4} [LinearOrderedAddCommMonoid γ] [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_4} [LinearOrderedAddCommMonoid γ] [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 α] {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 ∈ 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_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [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_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [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_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, LowerSemicontinuous (f i)) : LowerSemicontinuous fun (z : α) => ∑ i ∈ a, 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 ∈ 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) : UpperSemicontinuousWithinAt f t x

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) : UpperSemicontinuousWithinAt f s x

theorem UpperSemicontinuousOn.upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {x : α} {s : Set α} (h : UpperSemicontinuousOn f s) (hx : x ∈ s) : UpperSemicontinuousWithinAt f s x

theorem UpperSemicontinuousOn.mono {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {s : Set α} {t : Set α} (h : UpperSemicontinuousOn f s) (hst : t ⊆ s) : UpperSemicontinuousOn f t

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 : α) : UpperSemicontinuousAt f x

theorem UpperSemicontinuous.upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} (h : UpperSemicontinuous f) (s : Set α) (x : α) : UpperSemicontinuousWithinAt f s x

theorem UpperSemicontinuous.upperSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} (h : UpperSemicontinuous f) (s : Set α) : UpperSemicontinuousOn f s

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 (s.indicator 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 (s.indicator 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 (s.indicator 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 (s.indicator 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 (s.indicator 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 (s.indicator 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 (s.indicator 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 (s.indicator 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 : β) : IsOpen (f ⁻¹' Set.Iio 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 : γ) : IsClosed (f ⁻¹' Set.Ici y)

theorem ContinuousWithinAt.upperSemicontinuousWithinAt {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : ContinuousWithinAt f s x) : UpperSemicontinuousWithinAt f s x

theorem ContinuousAt.upperSemicontinuousAt {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : ContinuousAt f x) : UpperSemicontinuousAt f x

theorem ContinuousOn.upperSemicontinuousOn {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : ContinuousOn f s) : UpperSemicontinuousOn f s

theorem Continuous.upperSemicontinuous {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [LinearOrder γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} (h : Continuous f) : UpperSemicontinuous f

Equivalent definitions

theorem upperSemicontinuousWithinAt_iff_limsup_le {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : α → γ} : UpperSemicontinuousWithinAt f s x ↔ Filter.limsup f (nhdsWithin x s) ≤ f x

theorem UpperSemicontinuousWithinAt.limsup_le {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {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_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : α → γ} : UpperSemicontinuousAt f x ↔ Filter.limsup f (nhds x) ≤ f x

theorem UpperSemicontinuousAt.limsup_le {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {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_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : α → γ} : UpperSemicontinuous f ↔ ∀ (x : α), Filter.limsup f (nhds x) ≤ f x

theorem UpperSemicontinuous.limsup_le {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {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_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {f : α → γ} : UpperSemicontinuousOn f s ↔ ∀ x ∈ s, Filter.limsup f (nhdsWithin x s) ≤ f x

theorem UpperSemicontinuousOn.limsup_le {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] {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 upperSemicontinuous_iff_IsClosed_hypograph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} : UpperSemicontinuous f ↔ IsClosed {p : α × γ | p.2 ≤ f p.1}

theorem UpperSemicontinuous.IsClosed_hypograph {α : Type u_1} [TopologicalSpace α] {γ : Type u_3} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] {f : α → γ} : UpperSemicontinuous f → IsClosed {p : α × γ | p.2 ≤ f p.1}

Alias of the forward direction of upperSemicontinuous_iff_IsClosed_hypograph.

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)

theorem UpperSemicontinuousAt.comp_continuousAt {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : α → β} {g : ι → α} {x : ι} (hf : UpperSemicontinuousAt f (g x)) (hg : ContinuousAt g x) : UpperSemicontinuousAt (fun (x : ι) => f (g x)) x

theorem UpperSemicontinuousAt.comp_continuousAt_of_eq {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : α → β} {g : ι → α} {y : α} {x : ι} (hf : UpperSemicontinuousAt f y) (hg : ContinuousAt g x) (hy : g x = y) : UpperSemicontinuousAt (fun (x : ι) => f (g x)) x

theorem UpperSemicontinuous.comp_continuous {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {ι : Type u_5} [TopologicalSpace ι] {f : α → β} {g : ι → α} (hf : UpperSemicontinuous f) (hg : Continuous g) : UpperSemicontinuous fun (x : ι) => f (g x)

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.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_4} [LinearOrderedAddCommMonoid γ] [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_4} [LinearOrderedAddCommMonoid γ] [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_4} [LinearOrderedAddCommMonoid γ] [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 α] {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 ∈ 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_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [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_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [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_3} {γ : Type u_4} [LinearOrderedAddCommMonoid γ] [TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, UpperSemicontinuous (f i)) : UpperSemicontinuous fun (z : α) => ∑ i ∈ a, 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 ∈ 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 : α → γ} : Continuous f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f