Theorems · Theorem · measure theory

measurable_iSup_of_lowerSemicontinuous

∀ {β : Type u_2} {δ : Type u_4} [inst : TopologicalSpace β] {mβ : MeasurableSpace β} [BorelSpace β]
  {mδ : MeasurableSpace δ} [inst_2 : CompleteLinearOrder β] [OrderTopology β] [SecondCountableTopology β] {ι : Type u_5}
  [inst : TopologicalSpace ι] [TopologicalSpace.SeparableSpace ι] {f : ι → δ → β},
  (∀ (t : ι), Measurable (f t)) → (∀ (x : δ), LowerSemicontinuous fun x_1 => f x_1 x) → Measurable (⨆ i, f i)

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceBorelSpaceCompleteLinearOrderOrderTopologySecondCountableTopologyTopologicalSpaceTopologicalSpace.SeparableSpace