Theorems · Theorem · general topology

lowerSemicontinuousWithinAt_ciSup

∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {ι : Sort u_4} {δ' : Type u_6}
  [inst_1 : ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'},
  (∀ᶠ (y : α) in nhdsWithin x s, BddAbove (Set.range fun i => f i y)) →
    (∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x) → LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x

Defined in

Mathlib.Topology.Semicontinuity.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceConditionallyCompleteLinearOrder