iSup_Prop — Mathlib

English

For a Prop p and a measurable function f: δ → α, the function b ↦ ⨆ _ : p, f(b) is measurable.

Русский

Для пропозиции p и измеримой функции f: δ→α функция b ↦ ⨆_p f(b) измерима.

LaTeX

$$∀ p, ∀ f, (Measurable f) → Measurable fun b => ⨆ _ : p, f b$$

Lean4

@[measurability, fun_prop]
theorem iSup_Prop {α} {mα : MeasurableSpace α} [ConditionallyCompleteLattice α] (p : Prop) {f : δ → α}
    (hf : Measurable f) : Measurable fun b => ⨆ _ : p, f b := by
  classical
  simp_rw [ciSup_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const

Похожие утверждения