Hemicontinuity

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

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}