Theorems · Theorem · general topology

LowerHemicontinuousAt.of_sequences

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

Defined in

Mathlib.Topology.Semicontinuity.Hemicontinuity

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceFilter.IsCountablyGenerated