Theorems · Theorem · general topology

LowerHemicontinuousAt.exists_seq_tendsto

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

Defined in

Mathlib.Topology.Semicontinuity.Hemicontinuity

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceFilter.IsCountablyGenerated