measurable_sup' — Mathlib

English

Let s be a nonempty Finset of indices and f(i): δ → α be measurable for all i ∈ s. Then the function a ↦ sup_{i ∈ s} f(i)(a) is measurable.

Русский

Пусть s — ненулевой конечный набор индексов и для каждого i ∈ s функция f(i): δ → α измерима. Тогда a ↦ sup_{i ∈ s} f(i)(a) измерима.

LaTeX

$$$s\neq\varnothing \ o\ (\forall i\in s,\ Measurable (f i)) \to\ Measurable (s.sup' hs f).$$$

Lean4

@[measurability]
theorem measurable_sup' {ι : Type*} {s : Finset ι} (hs : s.Nonempty) {f : ι → δ → α} (hf : ∀ n ∈ s, Measurable (f n)) :
    Measurable (s.sup' hs f) :=
  Finset.sup'_induction hs _ (fun _f hf _g hg => hf.sup hg) fun n hn => hf n hn

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