measurable_range_sup'' — Mathlib

English

For f: ℕ → δ → α and n ∈ ℕ, if ∀ k ≤ n, f(k) is measurable, then the function x ↦ (range (n+1)).sup' ⋯ (fun k => f(k) x) is measurable.

Русский

Для f: ℕ → δ → α и n ∈ ℕ, если для каждого k ≤ n функция f(k) измерима, то x ↦ (range (n+1)).sup' ⋯ (fun k => f(k) x) измерима.

LaTeX

$$$(\forall k \le n, Measurable (f k)) \Rightarrow Measurable (x \mapsto (range (n+1)).sup' nonempty_range_add_one (fun k => f k x)).$$$

Lean4

@[measurability]
theorem measurable_range_sup'' {f : ℕ → δ → α} {n : ℕ} (hf : ∀ k ≤ n, Measurable (f k)) :
    Measurable fun x => (range (n + 1)).sup' nonempty_range_add_one fun k => f k x :=
  by
  convert Finset.measurable_range_sup' hf using 1
  ext x
  simp

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