Theorems · Theorem · general topology

lowerSemicontinuousOn_ciSup

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

Defined in

Mathlib.Topology.Semicontinuity.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceConditionallyCompleteLinearOrder