Theorems · Theorem · general topology

UpperHemicontinuousAt.of_sequences

∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x₀ : α}
  [(nhds x₀).IsCountablyGenerated] {K : Set β},
  IsSeqCompact K →
    (∀ᶠ (x : α) in nhds x₀, f x ⊆ K) →
      (∀ (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.

Defined in

Mathlib.Topology.Semicontinuity.Hemicontinuity

Cited by

1 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceFilter.IsCountablyGenerated