sSup — Mathlib

English

If s is countable and each f_i is measurable, then the function b ↦ ⨆ i∈s f_i b is measurable.

Русский

Если s счетно и каждая f_i измерима, то функция b ↦ ⨆ i∈s f_i b измерима.

LaTeX

$$s.Countable → (∀ i, Measurable (f i)) → Measurable fun b => ⨆ i ∈ s, f i b$$

Lean4

protected theorem sSup {ι} {f : ι → δ → α} {s : Set ι} (hs : s.Countable) (hf : ∀ i ∈ s, Measurable (f i)) :
    Measurable fun x => sSup ((fun i => f i x) '' s) :=
  by
  simp_rw [image_eq_range]
  have : Countable s := hs.to_subtype
  exact .iSup fun i ↦ hf i i.2

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