∀ {α : Type u_5} {β : Type u_6} {ι : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [RegularSpace β] {f : α → Set β} {x₀ : α} {l : Filter ι},
  UpperHemicontinuousAt f x₀ →
    IsClosed (f x₀) →
      ∀ {x : ι → α},
        Filter.Tendsto x l (nhds x₀) →
          ∀ {y : ι → β}, (∃ᶠ (n : ι) in l, y n ∈ f (x n)) → ∀ {y₀ : β}, Filter.Tendsto y l (nhds y₀) → y₀ ∈ f x₀