Hemicontinuity

This files provides basic facts about upper and lower hemicontinuity of correspondences f : α → Set β.

Basic facts

theorem upperHemicontinuousWithinAt_iff_forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {s : Set α} {x : α} [TopologicalSpace β] : UpperHemicontinuousWithinAt f s x ↔ ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ u

theorem UpperHemicontinuousWithinAt.of_forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {s : Set α} {x : α} [TopologicalSpace β] : (∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ u) → UpperHemicontinuousWithinAt f s x

Alias of the reverse direction of upperHemicontinuousWithinAt_iff_forall_isOpen.

theorem UpperHemicontinuousWithinAt.forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {s : Set α} {x : α} [TopologicalSpace β] : UpperHemicontinuousWithinAt f s x → ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ u

Alias of the forward direction of upperHemicontinuousWithinAt_iff_forall_isOpen.

theorem upperHemicontinuousOn_iff_forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {s : Set α} [TopologicalSpace β] : UpperHemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ u

theorem UpperHemicontinuousOn.forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {s : Set α} [TopologicalSpace β] : UpperHemicontinuousOn f s → ∀ x ∈ s, ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ u

Alias of the forward direction of upperHemicontinuousOn_iff_forall_isOpen.

theorem UpperHemicontinuousOn.of_forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {s : Set α} [TopologicalSpace β] : (∀ x ∈ s, ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ u) → UpperHemicontinuousOn f s

Alias of the reverse direction of upperHemicontinuousOn_iff_forall_isOpen.

theorem upperHemicontinuousAt_iff_forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {x : α} [TopologicalSpace β] : UpperHemicontinuousAt f x ↔ ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u

theorem UpperHemicontinuousAt.forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {x : α} [TopologicalSpace β] : UpperHemicontinuousAt f x → ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u

Alias of the forward direction of upperHemicontinuousAt_iff_forall_isOpen.

theorem UpperHemicontinuousAt.of_forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {x : α} [TopologicalSpace β] : (∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u) → UpperHemicontinuousAt f x

Alias of the reverse direction of upperHemicontinuousAt_iff_forall_isOpen.

theorem upperHemicontinuous_iff_forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} [TopologicalSpace β] : UpperHemicontinuous f ↔ ∀ (x : α) (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u

theorem UpperHemicontinuous.forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} [TopologicalSpace β] : UpperHemicontinuous f → ∀ (x : α) (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u

Alias of the forward direction of upperHemicontinuous_iff_forall_isOpen.

theorem UpperHemicontinuous.of_forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} [TopologicalSpace β] : (∀ (x : α) (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u) → UpperHemicontinuous f

Alias of the reverse direction of upperHemicontinuous_iff_forall_isOpen.

Characterization in terms of preimages of intervals of sets

theorem upperHemicontinuousWithinAt_iff_preimage_Iic {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {s : Set α} {x : α} [TopologicalSpace β] : UpperHemicontinuousWithinAt f s x ↔ ∀ u ∈ nhdsSet (f x), f ⁻¹' Set.Iic u ∈ nhdsWithin x s

theorem upperHemicontinuousAt_iff_preimage_Iic {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {x : α} [TopologicalSpace β] : UpperHemicontinuousAt f x ↔ ∀ u ∈ nhdsSet (f x), f ⁻¹' Set.Iic u ∈ nhds x

theorem upperHemicontinuousOn_iff_preimage_Iic {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {s : Set α} [TopologicalSpace β] : UpperHemicontinuousOn f s ↔ ∀ x ∈ s, ∀ u ∈ nhdsSet (f x), f ⁻¹' Set.Iic u ∈ nhdsWithin x s

theorem upperHemicontinuous_iff_preimage_Iic {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} [TopologicalSpace β] : UpperHemicontinuous f ↔ ∀ (x : α), ∀ u ∈ nhdsSet (f x), f ⁻¹' Set.Iic u ∈ nhds x

theorem upperHemicontinuous_iff_isOpen_preimage_Iic {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} [TopologicalSpace β] : UpperHemicontinuous f ↔ ∀ (u : Set β), IsOpen u → IsOpen (f ⁻¹' Set.Iic u)

A correspondence f : α → Set β is upper hemicontinuous if and only if its upper inverse (i.e., u : Set β ↦ f ⁻¹' (Iic u), note that f ⁻¹' (Iic u) = {x | f x ⊆ u}) sends open sets to open sets.

theorem upperHemicontinuous_iff_isClosed_compl_preimage_Iic_compl {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} [TopologicalSpace β] : UpperHemicontinuous f ↔ ∀ (u : Set β), IsClosed u → IsClosed (f ⁻¹' Set.Iic uᶜ)ᶜ

A correspondence f : α → Set β is upper hemicontinuous if and only if its lower inverse (i.e., u : Set β ↦ (f ⁻¹' (Iic uᶜ))ᶜ, note that f ⁻¹' (Iic u) = {x | (f x ∩ u).Nonempty}) sends closed sets to closed sets.

theorem isClosedMap_iff_upperHemicontinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} : IsClosedMap f ↔ UpperHemicontinuous fun (x : β) => f ⁻¹' {x}

theorem lowerHemicontinuous_iff_isOpen_inter_nonempty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} [TopologicalSpace β] : LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen u → IsOpen {x : α | (f x ∩ u).Nonempty}

theorem lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} [TopologicalSpace β] : LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen u → IsOpen (f ⁻¹' Set.Iic uᶜ)ᶜ

A correspondence f : α → Set β is lower hemicontinuous if and only if its lower inverse (i.e., u : Set β ↦ (f ⁻¹' (Iic uᶜ))ᶜ, note that f ⁻¹' (Iic u) = {x | (f x ∩ u).Nonempty}) sends open sets to open sets.

theorem lowerHemicontinuous_iff_isClosed_preimage_Iic {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} [TopologicalSpace β] : LowerHemicontinuous f ↔ ∀ (u : Set β), IsClosed u → IsClosed (f ⁻¹' Set.Iic u)

A correspondence f : α → Set β is lower hemicontinuous if and only if its upper inverse (i.e., u : Set β ↦ f ⁻¹' (Iic u), note that f ⁻¹' (Iic u) = {x | f x ⊆ u}) sends closed sets to closed sets.

theorem isOpenMap_iff_lowerHemicontinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} : IsOpenMap f ↔ LowerHemicontinuous fun (x : β) => f ⁻¹' {x}

Singleton maps

Functions f : α → β are continuous if and only if they are lower hemicontinuous if and only if they are upper hemicontinuous. This is in the sense that the map g : α → Set β given by g x = {f x} is both lower or upper hemicontinuous.

This section also provides dot notation to access this fact for continuous functions.

theorem upperHemicontinuous_singleton_id {α : Type u_1} [TopologicalSpace α] : UpperHemicontinuous fun (x : α) => {x}

@[simp]

theorem upperHemicontinuousWithinAt_singleton_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} : UpperHemicontinuousWithinAt (fun (x : α) => {f x}) s x ↔ ContinuousWithinAt f s x

theorem ContinuousWithinAt.upperHemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} : ContinuousWithinAt f s x → UpperHemicontinuousWithinAt (fun (x : α) => {f x}) s x

Alias of the reverse direction of upperHemicontinuousWithinAt_singleton_iff.

@[simp]

theorem upperHemicontinuousAt_singleton_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} : UpperHemicontinuousAt (fun (x : α) => {f x}) x ↔ ContinuousAt f x

theorem ContinuousAt.upperHemicontinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} : ContinuousAt f x → UpperHemicontinuousAt (fun (x : α) => {f x}) x

Alias of the reverse direction of upperHemicontinuousAt_singleton_iff.

@[simp]

theorem upperHemicontinuousOn_singleton_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} : UpperHemicontinuousOn (fun (x : α) => {f x}) s ↔ ContinuousOn f s

theorem ContinuousOn.upperHemicontinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} : ContinuousOn f s → UpperHemicontinuousOn (fun (x : α) => {f x}) s

Alias of the reverse direction of upperHemicontinuousOn_singleton_iff.

@[simp]

theorem upperHemicontinuous_singleton_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} : (UpperHemicontinuous fun (x : α) => {f x}) ↔ Continuous f

theorem Continuous.upperHemicontinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} : Continuous f → UpperHemicontinuous fun (x : α) => {f x}

Alias of the reverse direction of upperHemicontinuous_singleton_iff.

theorem lowerHemicontinuous_singleton_id {α : Type u_1} [TopologicalSpace α] : LowerHemicontinuous fun (x : α) => {x}

@[simp]

theorem lowerHemicontinuousWithinAt_singleton_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} : LowerHemicontinuousWithinAt (fun (x : α) => {f x}) s x ↔ ContinuousWithinAt f s x

theorem ContinuousWithinAt.lowerHemicontinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} : ContinuousWithinAt f s x → LowerHemicontinuousWithinAt (fun (x : α) => {f x}) s x

Alias of the reverse direction of lowerHemicontinuousWithinAt_singleton_iff.

@[simp]

theorem lowerHemicontinuousAt_singleton_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} : LowerHemicontinuousAt (fun (x : α) => {f x}) x ↔ ContinuousAt f x

theorem ContinuousAt.lowerHemicontinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} : ContinuousAt f x → LowerHemicontinuousAt (fun (x : α) => {f x}) x

Alias of the reverse direction of lowerHemicontinuousAt_singleton_iff.

@[simp]

theorem lowerHemicontinuousOn_singleton_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} : LowerHemicontinuousOn (fun (x : α) => {f x}) s ↔ ContinuousOn f s

theorem ContinuousOn.lowerHemicontinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} : ContinuousOn f s → LowerHemicontinuousOn (fun (x : α) => {f x}) s

Alias of the reverse direction of lowerHemicontinuousOn_singleton_iff.

@[simp]

theorem lowerHemicontinuous_singleton_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} : (LowerHemicontinuous fun (x : α) => {f x}) ↔ Continuous f

theorem Continuous.lowerHemicontinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} : Continuous f → LowerHemicontinuous fun (x : α) => {f x}

Alias of the reverse direction of lowerHemicontinuous_singleton_iff.

Union and intersection, and post-composition with the preimage map

theorem UpperHemicontinuousWithinAt.union {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f g : α → Set β} {s : Set α} {x : α} (hf : UpperHemicontinuousWithinAt f s x) (hg : UpperHemicontinuousWithinAt g s x) : UpperHemicontinuousWithinAt (fun (x : α) => f x ∪ g x) s x

Pointwise unions of upper hemicontinuous maps are upper hemicontinuous.

theorem UpperHemicontinuousOn.union {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f g : α → Set β} {s : Set α} (hf : UpperHemicontinuousOn f s) (hg : UpperHemicontinuousOn g s) : UpperHemicontinuousOn (fun (x : α) => f x ∪ g x) s

Pointwise unions of upper hemicontinuous maps are upper hemicontinuous.

theorem UpperHemicontinuousAt.union {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f g : α → Set β} {x : α} (hf : UpperHemicontinuousAt f x) (hg : UpperHemicontinuousAt g x) : UpperHemicontinuousAt (fun (x : α) => f x ∪ g x) x

Pointwise unions of upper hemicontinuous maps are upper hemicontinuous.

theorem UpperHemicontinuous.union {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f g : α → Set β} (hf : UpperHemicontinuous f) (hg : UpperHemicontinuous g) : UpperHemicontinuous fun (x : α) => f x ∪ g x

Pointwise unions of upper hemicontinuous maps are upper hemicontinuous.

theorem UpperHemicontinuousWithinAt.inter {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} {x : α} (hf : UpperHemicontinuousWithinAt f s x) {u : Set β} (hu : IsClosed u) : UpperHemicontinuousWithinAt (fun (x : α) => f x ∩ u) s x

The pointwise intersection of an upper hemicontinuous function with a fixed closed set is upper hemicontinuous.

theorem UpperHemicontinuousOn.inter {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} (hf : UpperHemicontinuousOn f s) {u : Set β} (hu : IsClosed u) : UpperHemicontinuousOn (fun (x : α) => f x ∩ u) s

The pointwise intersection of an upper hemicontinuous function with a fixed closed set is upper hemicontinuous.

theorem UpperHemicontinuousAt.inter {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} (hf : UpperHemicontinuousAt f x) {u : Set β} (hu : IsClosed u) : UpperHemicontinuousAt (fun (x : α) => f x ∩ u) x

The pointwise intersection of an upper hemicontinuous function with a fixed closed set is upper hemicontinuous.

theorem UpperHemicontinuous.inter {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} (hf : UpperHemicontinuous f) {u : Set β} (hu : IsClosed u) : UpperHemicontinuous fun (x : α) => f x ∩ u

The pointwise intersection of an upper hemicontinuous function with a fixed closed set is upper hemicontinuous.

theorem UpperHemicontinuousWithinAt.isInducing_comp {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} {x : α} {γ : Type u_5} [TopologicalSpace γ] {i : γ → β} (hf : UpperHemicontinuousWithinAt f s x) (hi : Topology.IsInducing i) (h_cl : IsClosed (Set.range i)) : UpperHemicontinuousWithinAt (fun (x : α) => i ⁻¹' f x) s x

Post-composition with the preimage of an inducing function whose range is closed preserves upper hemicontinuity.

theorem UpperHemicontinuousOn.isInducing_comp {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} {γ : Type u_5} [TopologicalSpace γ] {i : γ → β} (hf : UpperHemicontinuousOn f s) (hi : Topology.IsInducing i) (h_cl : IsClosed (Set.range i)) : UpperHemicontinuousOn (fun (x : α) => i ⁻¹' f x) s

Post-composition with the preimage of an inducing function whose range is closed preserves upper hemicontinuity.

theorem UpperHemicontinuousAt.isInducing_comp {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} {γ : Type u_5} [TopologicalSpace γ] {i : γ → β} (hf : UpperHemicontinuousAt f x) (hi : Topology.IsInducing i) (h_cl : IsClosed (Set.range i)) : UpperHemicontinuousAt (fun (x : α) => i ⁻¹' f x) x

Post-composition with the preimage of an inducing function whose range is closed preserves upper hemicontinuity.

theorem UpperHemicontinuous.isInducing_comp {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {γ : Type u_5} [TopologicalSpace γ] {i : γ → β} (hf : UpperHemicontinuous f) (hi : Topology.IsInducing i) (h_cl : IsClosed (Set.range i)) : UpperHemicontinuous fun (x : α) => i ⁻¹' f x

Post-composition with the preimage of an inducing function whose range is closed preserves upper hemicontinuity.

theorem UpperHemicontinuous.isClosed_domain {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} (hf : UpperHemicontinuous f) : IsClosed {x : α | (f x).Nonempty}

Upper hemicontinuous functions always have closed domain.

The more general fact is that if f is upper hemicontinuous at x₀ within s, and if x₀ is a cluster point of s ∩ {x | (f x).Nonempty}, then (f x₀).Nonempty.

Sequential characterizations

theorem UpperHemicontinuousAt.of_sequences {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x₀ : α} [(nhds x₀).IsCountablyGenerated] {K : Set β} (hK : IsSeqCompact K) (hf : ∀ᶠ (x : α) in nhds x₀, f x ⊆ K) (h : ∀ (x : ℕ → α), Filter.Tendsto x Filter.atTop (nhds x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Filter.Tendsto y Filter.atTop (nhds y₀) → y₀ ∈ f x₀) : UpperHemicontinuousAt f x₀

Sequential characterization of upper hemicontinuity: A set-valued function f : α → Set β is upper hemicontinuous at x₀ : α if for every pair of sequences x : ℕ → α and y : ℕ → β such that x tends to x₀ and y n ∈ f (x n) and y tends to y₀ : β, then y₀ ∈ f x₀. This requires that there is some (sequentially) compact set containing all f x' for x' sufficiently close to x.

This is a partial converse of UpperHemicontinuousAt.mem_of_tendsto.

theorem UpperHemicontinuousAt.mem_of_tendsto {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {ι : Type u_5} [RegularSpace β] {x₀ : α} {l : Filter ι} (hf : UpperHemicontinuousAt f x₀) (hf_closed : IsClosed (f x₀)) {x : ι → α} (hx : Filter.Tendsto x l (nhds x₀)) {y : ι → β} (hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)) {y₀ : β} (hy₀ : Filter.Tendsto y l (nhds y₀)) : y₀ ∈ f x₀

Sequential characterization of upper hemicontinuity: If β is a regular space and f : α → Set β is upper hemicontinuous at x₀ and f x₀ is closed, then for any sequences x and y (in α and β, respectively) tending to x₀ and y₀, respectively, if y n ∈ f (x n) frequently, then y₀ ∈ f x₀.

This is a partial converse of UpperHemicontinuousAt.of_sequences.

theorem LowerHemicontinuousAt.of_sequences {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x₀ : α} [(nhds x₀).IsCountablyGenerated] (h : ∀ (x : ℕ → α), Filter.Tendsto x Filter.atTop (nhds x₀) → ∀ y₀ ∈ f x₀, ∃ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) ∧ Filter.Tendsto y Filter.atTop (nhds y₀)) : LowerHemicontinuousAt f x₀

Sequential characterization of lower hemicontinuity: A set-valued function f : α → Set β is lower hemicontinuous at x₀ : α if for every sequence x : ℕ → α tending to x₀ and every y₀ ∈ f x₀, there exists a sequence y : ℕ → β with y n ∈ f (x n) for all n that tends to y₀.

theorem LowerHemicontinuousAt.exists_seq_tendsto {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x₀ : α} (hf : LowerHemicontinuousAt f x₀) {x : ℕ → α} (hx : Filter.Tendsto x Filter.atTop (nhds x₀)) {y₀ : β} (hy₀ : y₀ ∈ f x₀) [(nhds y₀).IsCountablyGenerated] : ∃ (y : ℕ → β), (∀ᶠ (n : ℕ) in Filter.atTop, y n ∈ f (x n)) ∧ Filter.Tendsto y Filter.atTop (nhds y₀)

Sequential characterization of lower hemicontinuity: If f : α → Set β is lower hemicontinuous at x₀, y₀ ∈ f x₀, 𝓝 y₀ is countably generated, and x : ℕ → α tends to x₀, then there is a companion sequence y : ℕ → β that tends to y₀ with y n ∈ f (x n) for all sufficiently large n.

This is a partial converse of LowerHemicontinuousAt.of_sequences.

theorem LowerHemicontinuousAt.exists_subseq_tendsto {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {ι : Type u_5} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] {x₀ : α} (hf : LowerHemicontinuousAt f x₀) {x : ι → α} (hx : Filter.Tendsto x l (nhds x₀)) {y₀ : β} (hy₀ : y₀ ∈ f x₀) [(nhds y₀).IsCountablyGenerated] : ∃ (u : ℕ → ι) (y : ℕ → β), Filter.Tendsto u Filter.atTop l ∧ (∀ᶠ (k : ℕ) in Filter.atTop, y k ∈ f (x (u k))) ∧ Filter.Tendsto y Filter.atTop (nhds y₀)

Lower hemicontinuity along a countably generated filter (subsequence form): if f : α → Set β is lower hemicontinuous at x₀, y₀ ∈ f x₀, 𝓝 y₀ is countably generated and x : ι → α tends to x₀ along a nontrivial countably generated filter l, then some sequence u : ℕ → ι converging to l admits a companion y : ℕ → β tending to y₀ with y k ∈ f (x (u k)) eventually.

For a general filter one must pass to the subsequence u: the "same-index" conclusion already fails for l = pure i₀ (which is NeBot and countably generated). When l = atTop one may take u = id, recovering LowerHemicontinuousAt.exists_seq_tendsto.

Open lower sections

theorem hasOpenLowerSections_iff_isOpen_compl_preimage_Iic_compl {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} : HasOpenLowerSections f ↔ ∀ (b : β), IsOpen (f ⁻¹' Set.Iic {b}ᶜ)ᶜ

A correspondence f : α → Set β has open lower sections if and only if its lower inverse (i.e., b : β ↦ (f ⁻¹' Iic {b}ᶜ)ᶜ = {x | b ∈ f x}) sends every point to an open set.

theorem hasOpenLowerSections_iff_isClosed_preimage_Iic {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} : HasOpenLowerSections f ↔ ∀ (b : β), IsClosed (f ⁻¹' Set.Iic {b}ᶜ)

A correspondence f : α → Set β has open lower sections if and only if its upper inverse (i.e., b : β ↦ f ⁻¹' (Iic {b}ᶜ) = {x | b ∉ f x}) sends every point to a closed set.

Open Graphs

theorem LowerHemicontinuous.inter_hasOpenCGraph {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → Set β} (hf : LowerHemicontinuous f) (hg : HasOpenCGraph g) : LowerHemicontinuous fun (x : α) => f x ∩ g x

A lower hemicontinuous function intersected with a function with an open graph is lower hemicontinuous.

Uniform Limits

Like continuity, hemicontinuity is preserved under certain uniform limits, where the uniformity on the target Set β is the Hausdorff uniformity. In this section, we prove this result for both lower hemicontinuous and upper hemicontinuous limits.

theorem TendstoUniformlyOn.lowerHemicontinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {s : Set α} {ι : Type u_3} {F : ι → α → Set β} {l : Filter ι} [l.NeBot] [UniformSpace β] (htendsto : TendstoUniformlyOn F f l s) (hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s) : LowerHemicontinuousOn f s

A net of lower hemicontinuous set-valued functions converging uniformly on s (along a filter l) in the Hausdorff uniformity has a lower hemicontinuous limit on s

theorem TendstoUniformlyOn.upperHemicontinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {s : Set α} {ι : Type u_3} {F : ι → α → Set β} {l : Filter ι} [l.NeBot] [UniformSpace β] (htendsto : TendstoUniformlyOn F f l s) (hF : ∀ (n : ι), UpperHemicontinuousOn (F n) s) (hf_compact : ∀ x ∈ s, IsCompact (f x)) : UpperHemicontinuousOn f s

If a net of upper hemicontinuous set-valued functions converges uniformly (along a filter l) in the Hausdorff uniformity to a set-valued function f with compact values, then f is upper hemicontinuous

theorem TendstoUniformly.lowerHemicontinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {ι : Type u_3} {F : ι → α → Set β} {l : Filter ι} [l.NeBot] [UniformSpace β] (htendsto : TendstoUniformly F f l) (hF : ∀ (n : ι), LowerHemicontinuous (F n)) : LowerHemicontinuous f

A net of lower hemicontinuous set-valued functions converging uniformly (along a filter l) in the Hausdorff uniformity has a lower hemicontinuous limit

theorem TendstoUniformly.upperHemicontinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → Set β} {ι : Type u_3} {F : ι → α → Set β} {l : Filter ι} [l.NeBot] [UniformSpace β] (htendsto : TendstoUniformly F f l) (hF : ∀ (n : ι), UpperHemicontinuous (F n)) (hf_compact : ∀ (x : α), IsCompact (f x)) : UpperHemicontinuous f

If a net of upper hemicontinuous set-valued functions converges uniformly (along a filter l) in the Hausdorff uniformity to a set-valued function f with compact values, then f is upper hemicontinuous