measurable_range_sup' — Mathlib

English

If hf(k) is measurable for all k ≤ n, then the function x ↦ (range (n+1)).sup' nonempty_range_add_one f evaluated at x is measurable.

Русский

Если для каждого k ≤ n функция f(k) измерима, то функция x ↦ (range (n+1)).sup' nonempty_range_add_one f (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 ((range (n + 1)).sup' nonempty_range_add_one f) :=
  by
  simp_rw [← Nat.lt_succ_iff] at hf
  refine Finset.measurable_sup' _ ?_
  simpa [Finset.mem_range]

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