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 α] [TopologicalSpace β] {f : α → Set β} {s : Set α} {x : α} : 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 α] [TopologicalSpace β] {f : α → Set β} {s : Set α} {x : α} : (∀ (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 α] [TopologicalSpace β] {f : α → Set β} {s : Set α} {x : α} : 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 α] [TopologicalSpace β] {f : α → Set β} {s : Set α} : 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 α] [TopologicalSpace β] {f : α → Set β} {s : Set α} : 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 α] [TopologicalSpace β] {f : α → Set β} {s : Set α} : (∀ 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 α] [TopologicalSpace β] {f : α → Set β} {x : α} : UpperHemicontinuousAt f x ↔ ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u

theorem UpperHemicontinuousAt.of_forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} : (∀ (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 UpperHemicontinuousAt.forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} : 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 upperHemicontinuous_iff_forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : UpperHemicontinuous f ↔ ∀ (x : α) (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u

theorem UpperHemicontinuous.of_forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : (∀ (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.

theorem UpperHemicontinuous.forall_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : 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.

Characterization in terms of preimages of intervals of sets

theorem upperHemicontinuousWithinAt_iff_preimage_Iic {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} {x : α} : 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 α] [TopologicalSpace β] {f : α → Set β} {x : α} : 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 α] [TopologicalSpace β] {f : α → Set β} {s : Set α} : 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 α] [TopologicalSpace β] {f : α → Set β} : 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 α] [TopologicalSpace β] {f : α → Set β} : 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 α] [TopologicalSpace β] {f : α → Set β} : 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_compl_preimage_Iic_compl {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : 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 α] [TopologicalSpace β] {f : α → Set β} : 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

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

@[simp]

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

@[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

@[simp]

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

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_5} {β : Type u_6} [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_5} {β : Type u_6} [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_5} {β : Type u_6} {ι : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [RegularSpace β] {f : α → Set β} {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.