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 cannot jump down.

Upper semicontinuous functions are defined similarly. Upper and lower hemicontinuity (of functions f : α → Set β) are often defined in terms of sequential characterizations, but here we take an equivalent approach. f : α → Set β is upper hemicontinuous at x if for any neighborhood of f x, f x' is included in this neighborhood for all x' close enough to x.

Of course, one can see a superficial similarity between upper semicontinuity and upper hemicontinuity. In fact, we can unify all of upper and lower semicontinuity and also upper and lower hemicontinuity under one umbrella, by considering a general relation r : α → β → Prop and defining semicontinuity of this relation.

This file introduces these notions, and a basic API around them mimicking the API for continuous functions.

Main definitions and results

We introduce 4 generic definitions related to semicontinuity:

• SemicontinuousWithinAt r s x
• SemicontinuousAt r x
• SemicontinuousOn r s
• Semicontinuous r

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

• constant functions are semicontinuous;
• right composition with continuous functions preserves semicontinuity;

We also define lower and upper semicontinuity as abbreviations of these generic definitions and transfer the generic results to these notions.

References

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

Main definitions

def SemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] (r : α → β → Prop) (s : Set α) (x : α) : Prop

A relation r : α → β → Prop is semicontinuous within s at x : α, if whenever r x y is true, it is also true for all x' sufficiently close to x within s.

This notion generalizes lower and upper semicontinuity of functions, as well as lower and upper hemicontinuity of set-valued correspondences.

Equations

• SemicontinuousWithinAt r s x = ∀ (y : β), r x y → ∀ᶠ (x' : α) in nhdsWithin x s, r x' y

def SemicontinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] (r : α → β → Prop) (s : Set α) : Prop

A relation r : α → β → Prop is semicontinuous on s if it is semicontinuous within s at each x ∈ s.

Equations

• SemicontinuousOn r s = ∀ x ∈ s, SemicontinuousWithinAt r s x

def SemicontinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] (r : α → β → Prop) (x : α) : Prop

A relation r : α → β → Prop is semicontinuous at x : α, if whenever r x y is true, it is also true for all x' sufficiently close to x.

This notion generalizes lower and upper semicontinuity of functions, as well as lower and upper hemicontinuity of set-valued correspondences.

Equations

• SemicontinuousAt r x = ∀ (y : β), r x y → ∀ᶠ (x' : α) in nhds x, r x' y

def Semicontinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] (r : α → β → Prop) : Prop

A relation r : α → β → Prop is semicontinuous if it is semicontinuous within s at each x : α.

Equations

• Semicontinuous r = ∀ (x : α), SemicontinuousAt r x

theorem SemicontinuousWithinAt.mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} {x : α} {s t : Set α} (h : SemicontinuousWithinAt r s x) (hst : t ⊆ s) : SemicontinuousWithinAt r t x

theorem SemicontinuousWithinAt.congr_of_eventuallyEq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r r' : α → β → Prop} {s : Set α} {a : α} (h : SemicontinuousWithinAt r s a) (has : a ∈ s) (hfg : ∀ᶠ (x : α) in nhdsWithin a s, ∀ (y : β), r x y ↔ r' x y) : SemicontinuousWithinAt r' s a

theorem semicontinuousWithinAt_univ_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} {x : α} : SemicontinuousWithinAt r Set.univ x ↔ SemicontinuousAt r x

theorem SemicontinuousAt.semicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} {x : α} (s : Set α) (h : SemicontinuousAt r x) : SemicontinuousWithinAt r s x

theorem SemicontinuousOn.semicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} {x : α} {s : Set α} (h : SemicontinuousOn r s) (hx : x ∈ s) : SemicontinuousWithinAt r s x

theorem SemicontinuousOn.mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} {s t : Set α} (h : SemicontinuousOn r s) (hst : t ⊆ s) : SemicontinuousOn r t

theorem semicontinuousOn_univ_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} : SemicontinuousOn r Set.univ ↔ Semicontinuous r

@[simp]

theorem semicontinuous_restrict_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} {s : Set α} : Semicontinuous (s.restrict r) ↔ SemicontinuousOn r s

theorem Semicontinuous.semicontinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} (h : Semicontinuous r) (x : α) : SemicontinuousAt r x

theorem Semicontinuous.semicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} (h : Semicontinuous r) (s : Set α) (x : α) : SemicontinuousWithinAt r s x

theorem Semicontinuous.semicontinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} (h : Semicontinuous r) (s : Set α) : SemicontinuousOn r s

Constants

theorem SemicontinuousWithinAt.const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {x : α} {s : Set α} {f : β → Prop} : SemicontinuousWithinAt (fun (_x : α) => f) s x

theorem SemicontinuousAt.const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {x : α} {f : β → Prop} : SemicontinuousAt (fun (_x : α) => f) x

theorem SemicontinuousOn.const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {s : Set α} {f : β → Prop} : SemicontinuousOn (fun (_x : α) => f) s

theorem Semicontinuous.const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : β → Prop} : Semicontinuous fun (_x : α) => f

Precomposition with a continuous map

theorem SemicontinuousWithinAt.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] {r : α → β → Prop} {x : γ} {g : γ → α} {s : Set γ} {t : Set α} (h : SemicontinuousWithinAt r t (g x)) (hg : ContinuousWithinAt g s x) (hst : Set.MapsTo g s t) : SemicontinuousWithinAt (r ∘ g) s x

theorem SemicontinuousOn.comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} {γ : Type u_4} [TopologicalSpace γ] {g : γ → α} {s : Set γ} {t : Set α} (h : SemicontinuousOn r t) (hg : ContinuousOn g s) (hst : Set.MapsTo g s t) : SemicontinuousOn (r ∘ g) s

theorem SemicontinuousAt.comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} {γ : Type u_4} [TopologicalSpace γ] {x : γ} {g : γ → α} (h : SemicontinuousAt r (g x)) (hg : ContinuousAt g x) : SemicontinuousAt (r ∘ g) x

theorem Semicontinuous.comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} {γ : Type u_4} [TopologicalSpace γ] {g : γ → α} (h : Semicontinuous r) (hg : Continuous g) : Semicontinuous (r ∘ g)

Lower and Upper Semicontinuity

@[reducible, inline]

abbrev LowerSemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [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 = SemicontinuousWithinAt (fun (x1 : α) (x2 : β) => f x1 > x2) s x

@[reducible, inline]

abbrev LowerSemicontinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [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 = SemicontinuousOn (fun (x1 : α) (x2 : β) => f x1 > x2) s

@[reducible, inline]

abbrev LowerSemicontinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [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 = SemicontinuousAt (fun (x1 : α) (x2 : β) => f x1 > x2) x

@[reducible, inline]

abbrev LowerSemicontinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [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 = Semicontinuous fun (x1 : α) (x2 : β) => f x1 > x2

@[reducible, inline]

abbrev UpperSemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [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 = SemicontinuousWithinAt (fun (x1 : α) (x2 : β) => f x1 < x2) s x

@[reducible, inline]

abbrev UpperSemicontinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [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 = SemicontinuousOn (fun (x1 : α) (x2 : β) => f x1 < x2) s

@[reducible, inline]

abbrev UpperSemicontinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [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 = SemicontinuousAt (fun (x1 : α) (x2 : β) => f x1 < x2) x

@[reducible, inline]

abbrev UpperSemicontinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [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 = Semicontinuous fun (x1 : α) (x2 : β) => f x1 < x2

theorem lowerSemicontinuousWithinAt_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} {s : Set α} {x : α} : LowerSemicontinuousWithinAt f s x ↔ ∀ y < f x, ∀ᶠ (x' : α) in nhdsWithin x s, y < f x'

theorem lowerSemicontinuousOn_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} {s : Set α} : LowerSemicontinuousOn f s ↔ ∀ x ∈ s, LowerSemicontinuousWithinAt f s x

theorem lowerSemicontinuousAt_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} {x : α} : LowerSemicontinuousAt f x ↔ ∀ y < f x, ∀ᶠ (x' : α) in nhds x, y < f x'

theorem lowerSemicontinuous_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} : LowerSemicontinuous f ↔ ∀ (x : α), LowerSemicontinuousAt f x

theorem upperSemicontinuousWithinAt_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} {s : Set α} {x : α} : UpperSemicontinuousWithinAt f s x ↔ ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhdsWithin x s, f x' < y

theorem upperSemicontinuousOn_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} {s : Set α} : UpperSemicontinuousOn f s ↔ ∀ x ∈ s, UpperSemicontinuousWithinAt f s x

theorem upperSemicontinuousAt_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} {x : α} : UpperSemicontinuousAt f x ↔ ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhds x, f x' < y

theorem upperSemicontinuous_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} : UpperSemicontinuous f ↔ ∀ (x : α), UpperSemicontinuousAt f x

Lower semicontinuous functions

Basic dot notation interface for lower semicontinuity

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

theorem LowerSemicontinuousWithinAt.congr_of_eventuallyEq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f g : α → β} {s : Set α} {a : α} (h : LowerSemicontinuousWithinAt f s a) (has : a ∈ s) (hfg : f =ᶠ[nhdsWithin a s] g) : LowerSemicontinuousWithinAt g s a

theorem lowerSemicontinuousWithinAt_univ_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} {x : α} : LowerSemicontinuousWithinAt f Set.univ x ↔ LowerSemicontinuousAt f x

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

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

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

theorem lowerSemicontinuousOn_univ_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} : LowerSemicontinuousOn f Set.univ ↔ LowerSemicontinuous f

@[simp]

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

theorem LowerSemicontinuous.lowerSemicontinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} (h : LowerSemicontinuous f) (x : α) : LowerSemicontinuousAt f x

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

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

Constants

theorem lowerSemicontinuousWithinAt_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {x : α} {s : Set α} {z : β} : LowerSemicontinuousWithinAt (fun (_x : α) => z) s x

theorem lowerSemicontinuousAt_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {x : α} {z : β} : LowerSemicontinuousAt (fun (_x : α) => z) x

theorem lowerSemicontinuousOn_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {s : Set α} {z : β} : LowerSemicontinuousOn (fun (_x : α) => z) s

theorem lowerSemicontinuous_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {z : β} : LowerSemicontinuous fun (_x : α) => z

Composition

theorem LowerSemicontinuousWithinAt.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [Preorder β] {f : α → β} {s : Set α} {g : γ → α} {x : γ} {t : Set γ} (hf : LowerSemicontinuousWithinAt f s (g x)) (hg : ContinuousWithinAt g t x) (hg' : Set.MapsTo g t s) : LowerSemicontinuousWithinAt (f ∘ g) t x

theorem LowerSemicontinuousAt.comp {α : 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

theorem LowerSemicontinuousOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [Preorder β] {f : α → β} {s : Set α} {g : γ → α} {t : Set γ} (hf : LowerSemicontinuousOn f s) (hg : ContinuousOn g t) (hg' : Set.MapsTo g t s) : LowerSemicontinuousOn (f ∘ g) t

theorem LowerSemicontinuous.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [Preorder β] {f : α → β} {g : γ → α} (hf : LowerSemicontinuous f) (hg : Continuous g) : LowerSemicontinuous (f ∘ g)

Upper semicontinuous functions

Basic dot notation interface for upper semicontinuity

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

theorem UpperSemicontinuousWithinAt.congr_of_eventuallyEq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f g : α → β} {s : Set α} {a : α} (h : UpperSemicontinuousWithinAt f s a) (has : a ∈ s) (hfg : ∀ᶠ (x : α) in nhdsWithin a s, f x = g x) : UpperSemicontinuousWithinAt g s a

theorem upperSemicontinuousWithinAt_univ_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} {x : α} : UpperSemicontinuousWithinAt f Set.univ x ↔ UpperSemicontinuousAt f x

@[simp]

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

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

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

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

theorem upperSemicontinuousOn_univ_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} : UpperSemicontinuousOn f Set.univ ↔ UpperSemicontinuous f

theorem UpperSemicontinuous.upperSemicontinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} (h : UpperSemicontinuous f) (x : α) : UpperSemicontinuousAt f x

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

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

Constants

theorem upperSemicontinuousWithinAt_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {x : α} {s : Set α} {z : β} : UpperSemicontinuousWithinAt (fun (_x : α) => z) s x

theorem upperSemicontinuousAt_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {x : α} {z : β} : UpperSemicontinuousAt (fun (_x : α) => z) x

theorem upperSemicontinuousOn_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {s : Set α} {z : β} : UpperSemicontinuousOn (fun (_x : α) => z) s

theorem upperSemicontinuous_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {z : β} : UpperSemicontinuous fun (_x : α) => z

Composition

theorem UpperSemicontinuousWithinAt.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [Preorder β] {f : α → β} {s : Set α} {g : γ → α} {c : γ} {t : Set γ} (hf : UpperSemicontinuousWithinAt f s (g c)) (hg : ContinuousWithinAt g t c) (hg' : Set.MapsTo g t s) : UpperSemicontinuousWithinAt (f ∘ g) t c

theorem UpperSemicontinuousAt.comp {α : 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

theorem UpperSemicontinuousOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [Preorder β] {f : α → β} {s : Set α} {g : γ → α} {t : Set γ} (hf : UpperSemicontinuousOn f s) (hg : ContinuousOn g t) (hg' : Set.MapsTo g t s) : UpperSemicontinuousOn (f ∘ g) t

theorem UpperSemicontinuous.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [Preorder β] {f : α → β} {g : γ → α} (hf : UpperSemicontinuous f) (hg : Continuous g) : UpperSemicontinuous (f ∘ g)

Lower and Upper Semicontinuity

@[reducible, inline]

abbrev LowerHemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → Set β) (s : Set α) (x : α) : Prop

A function f : α → Set β is lower hemicontinuous at x within a set s if, whenever t is an open set intersecting f x, then t also intersects f x' for all x' sufficiently close to x within s.

Equations

• LowerHemicontinuousWithinAt f s x = SemicontinuousWithinAt (fun (x : α) (t : Set β) => IsOpen t ∧ (f x ∩ t).Nonempty) s x

@[reducible, inline]

abbrev LowerHemicontinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → Set β) (s : Set α) : Prop

A function f : α → Set β is lower hemicontinuous on a set s if, whenever x ∈ s and t is an open set intersecting f x, then t also intersects f x' for all x' sufficiently close to x within s.

Equations

• LowerHemicontinuousOn f s = SemicontinuousOn (fun (x : α) (t : Set β) => IsOpen t ∧ (f x ∩ t).Nonempty) s

@[reducible, inline]

abbrev LowerHemicontinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → Set β) (x : α) : Prop

A function f : α → Set β is lower hemicontinuous at x if, whenever t is an open set intersecting f x, then t also intersects f x' for all x' sufficiently close to x.

Equations

• LowerHemicontinuousAt f x = SemicontinuousAt (fun (x : α) (t : Set β) => IsOpen t ∧ (f x ∩ t).Nonempty) x

@[reducible, inline]

abbrev LowerHemicontinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → Set β) : Prop

A function f : α → Set β is lower hemicontinuous if, for any x, whenever t is an open set intersecting f x, then t also intersects f x' for all x' sufficiently close to x.

Equations

• LowerHemicontinuous f = Semicontinuous fun (x : α) (t : Set β) => IsOpen t ∧ (f x ∩ t).Nonempty

@[reducible, inline]

abbrev UpperHemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → Set β) (s : Set α) (x : α) : Prop

A function f : α → Set β is upper hemicontinuous at x within a set s if, whenever t is a neighborhood of f x, then t is a neighborhood of f x' for all x' sufficiently close to x within s.

Equations

• UpperHemicontinuousWithinAt f s x = SemicontinuousWithinAt (fun (x : α) (t : Set β) => t ∈ nhdsSet (f x)) s x

@[reducible, inline]

abbrev UpperHemicontinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → Set β) (s : Set α) : Prop

A function f : α → Set β is upper hemicontinuous on a set s if, whenever x ∈ s and t is a neighborhood of f x, then t is a neighborhood of f x' for all x' sufficiently close to x within s.

Equations

• UpperHemicontinuousOn f s = SemicontinuousOn (fun (x : α) (t : Set β) => t ∈ nhdsSet (f x)) s

@[reducible, inline]

abbrev UpperHemicontinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → Set β) (x : α) : Prop

A function f : α → Set β is upper hemicontinuous at x if, whenever t is a neighborhood of f x, then t is a neighborhood of f x' for all x' sufficiently close to x.

Equations

• UpperHemicontinuousAt f x = SemicontinuousAt (fun (x : α) (t : Set β) => t ∈ nhdsSet (f x)) x

@[reducible, inline]

abbrev UpperHemicontinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → Set β) : Prop

A function f : α → Set β is upper hemicontinuous if, for all x, whenever t is a neighborhood of f x, then t is a neighborhood of f x' for all x' sufficiently close to x.

Equations

• UpperHemicontinuous f = Semicontinuous fun (x : α) (t : Set β) => t ∈ nhdsSet (f x)

theorem lowerHemicontinuousWithinAt_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} {x : α} : LowerHemicontinuousWithinAt f s x ↔ ∀ (u : Set β), IsOpen u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in nhdsWithin x s, (f x' ∩ u).Nonempty

theorem lowerHemicontinuousOn_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} : LowerHemicontinuousOn f s ↔ ∀ x ∈ s, LowerHemicontinuousWithinAt f s x

theorem lowerHemicontinuousAt_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} : LowerHemicontinuousAt f x ↔ ∀ (u : Set β), IsOpen u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in nhds x, (f x' ∩ u).Nonempty

theorem lowerHemicontinuous_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : LowerHemicontinuous f ↔ ∀ (x : α), LowerHemicontinuousAt f x

theorem upperHemicontinuousWithinAt_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} {x : α} : UpperHemicontinuousWithinAt f s x ↔ ∀ t ∈ nhdsSet (f x), ∀ᶠ (x' : α) in nhdsWithin x s, t ∈ nhdsSet (f x')

theorem upperHemicontinuousOn_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} : UpperHemicontinuousOn f s ↔ ∀ x ∈ s, UpperHemicontinuousWithinAt f s x

theorem upperHemicontinuousAt_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} : UpperHemicontinuousAt f x ↔ ∀ t ∈ nhdsSet (f x), ∀ᶠ (x' : α) in nhds x, t ∈ nhdsSet (f x')

theorem upperHemicontinuous_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : UpperHemicontinuous f ↔ ∀ (x : α), UpperHemicontinuousAt f x

Lower semicontinuous functions

Basic dot notation interface for lower semicontinuity

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

theorem LowerHemicontinuousWithinAt.congr_of_eventuallyEq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → Set β} {s : Set α} {a : α} (h : LowerHemicontinuousWithinAt f s a) (has : a ∈ s) (hfg : f =ᶠ[nhdsWithin a s] g) : LowerHemicontinuousWithinAt g s a

theorem lowerHemicontinuousWithinAt_univ_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} : LowerHemicontinuousWithinAt f Set.univ x ↔ LowerHemicontinuousAt f x

theorem LowerHemicontinuousAt.lowerHemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} (s : Set α) (h : LowerHemicontinuousAt f x) : LowerHemicontinuousWithinAt f s x

theorem LowerHemicontinuousOn.lowerHemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} {s : Set α} (h : LowerHemicontinuousOn f s) (hx : x ∈ s) : LowerHemicontinuousWithinAt f s x

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

theorem lowerHemicontinuousOn_univ_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : LowerHemicontinuousOn f Set.univ ↔ LowerHemicontinuous f

@[simp]

theorem lowerHemicontinuous_restrict_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} : LowerHemicontinuous (s.restrict f) ↔ LowerHemicontinuousOn f s

theorem LowerHemicontinuous.lowerHemicontinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} (h : LowerHemicontinuous f) (x : α) : LowerHemicontinuousAt f x

theorem LowerHemicontinuous.lowerHemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} (h : LowerHemicontinuous f) (s : Set α) (x : α) : LowerHemicontinuousWithinAt f s x

theorem LowerHemicontinuous.lowerHemicontinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} (h : LowerHemicontinuous f) (s : Set α) : LowerHemicontinuousOn f s

Constants

theorem LowerHemicontinuousWithinAt.const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {x : α} {s : Set α} {z : Set β} : LowerHemicontinuousWithinAt (fun (_x : α) => z) s x

theorem LowerHemicontinuousAt.const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {x : α} {z : Set β} : LowerHemicontinuousAt (fun (_x : α) => z) x

theorem LowerHemicontinuousOn.const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {z : Set β} : LowerHemicontinuousOn (fun (_x : α) => z) s

theorem LowerHemicontinuous.const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {z : Set β} : LowerHemicontinuous fun (_x : α) => z

Composition

theorem LowerHemicontinuousWithinAt.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [TopologicalSpace β] {f : α → Set β} {s : Set α} {g : γ → α} {x : γ} {t : Set γ} (hf : LowerHemicontinuousWithinAt f s (g x)) (hg : ContinuousWithinAt g t x) (hg' : Set.MapsTo g t s) : LowerHemicontinuousWithinAt (f ∘ g) t x

theorem LowerHemicontinuousAt.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [TopologicalSpace β] {f : α → Set β} {g : γ → α} {x : γ} (hf : LowerHemicontinuousAt f (g x)) (hg : ContinuousAt g x) : LowerHemicontinuousAt (f ∘ g) x

theorem LowerHemicontinuousOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [TopologicalSpace β] {f : α → Set β} {s : Set α} {g : γ → α} {t : Set γ} (hf : LowerHemicontinuousOn f s) (hg : ContinuousOn g t) (hg' : Set.MapsTo g t s) : LowerHemicontinuousOn (f ∘ g) t

theorem LowerHemicontinuous.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [TopologicalSpace β] {f : α → Set β} {g : γ → α} (hf : LowerHemicontinuous f) (hg : Continuous g) : LowerHemicontinuous (f ∘ g)

Upper semicontinuous functions

Basic dot notation interface for upper semicontinuity

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

theorem UpperHemicontinuousWithinAt.congr_of_eventuallyEq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → Set β} {s : Set α} {a : α} (h : UpperHemicontinuousWithinAt f s a) (has : a ∈ s) (hfg : ∀ᶠ (x : α) in nhdsWithin a s, f x = g x) : UpperHemicontinuousWithinAt g s a

theorem upperHemicontinuousWithinAt_univ_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} : UpperHemicontinuousWithinAt f Set.univ x ↔ UpperHemicontinuousAt f x

@[simp]

theorem upperHemicontinuousOn_iff_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} : UpperHemicontinuous (s.restrict f) ↔ UpperHemicontinuousOn f s

theorem UpperHemicontinuousAt.upperHemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} (s : Set α) (h : UpperHemicontinuousAt f x) : UpperHemicontinuousWithinAt f s x

theorem UpperHemicontinuousOn.upperHemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} {s : Set α} (h : UpperHemicontinuousOn f s) (hx : x ∈ s) : UpperHemicontinuousWithinAt f s x

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

theorem upperHemicontinuousOn_univ_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : UpperHemicontinuousOn f Set.univ ↔ UpperHemicontinuous f

theorem UpperHemicontinuous.upperHemicontinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} (h : UpperHemicontinuous f) (x : α) : UpperHemicontinuousAt f x

theorem UpperHemicontinuous.upperHemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} (h : UpperHemicontinuous f) (s : Set α) (x : α) : UpperHemicontinuousWithinAt f s x

theorem UpperHemicontinuous.upperHemicontinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} (h : UpperHemicontinuous f) (s : Set α) : UpperHemicontinuousOn f s

Constants

theorem UpperHemicontinuousWithinAt.const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {x : α} {s : Set α} {z : Set β} : UpperHemicontinuousWithinAt (fun (_x : α) => z) s x

theorem UpperHemicontinuousAt.const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {x : α} {z : Set β} : UpperHemicontinuousAt (fun (_x : α) => z) x

theorem UpperHemicontinuousOn.const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {z : Set β} : UpperHemicontinuousOn (fun (_x : α) => z) s

theorem UpperHemicontinuous.const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {z : Set β} : UpperHemicontinuous fun (_x : α) => z

Composition

theorem UpperHemicontinuousWithinAt.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [TopologicalSpace β] {f : α → Set β} {s : Set α} {g : γ → α} {c : γ} {t : Set γ} (hf : UpperHemicontinuousWithinAt f s (g c)) (hg : ContinuousWithinAt g t c) (hg' : Set.MapsTo g t s) : UpperHemicontinuousWithinAt (f ∘ g) t c

theorem UpperHemicontinuousAt.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [TopologicalSpace β] {f : α → Set β} {g : γ → α} {c : γ} (hf : UpperHemicontinuousAt f (g c)) (hg : ContinuousAt g c) : UpperHemicontinuousAt (f ∘ g) c

theorem UpperHemicontinuousOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [TopologicalSpace β] {f : α → Set β} {s : Set α} {g : γ → α} {t : Set γ} (hf : UpperHemicontinuousOn f s) (hg : ContinuousOn g t) (hg' : Set.MapsTo g t s) : UpperHemicontinuousOn (f ∘ g) t

theorem UpperHemicontinuous.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace γ] [TopologicalSpace β] {f : α → Set β} {g : γ → α} (hf : UpperHemicontinuous f) (hg : Continuous g) : UpperHemicontinuous (f ∘ g)