sInf — Mathlib

English

If s is countable and each f_i is measurable, then the supremum over s of f_i(x) is measurable in x.

Русский

Если s счетно и каждая f_i измерима, то супремум по i∈s f_i(x) измерим по x.

LaTeX

$$s.Countable → (∀ i ∈ s, Measurable (f i)) → Measurable fun x => sSup ((fun i => f i x) '' s)$$

Lean4

protected theorem sInf {ι} {f : ι → δ → α} {s : Set ι} (hs : s.Countable) (hf : ∀ i ∈ s, Measurable (f i)) :
    Measurable fun x => sInf ((fun i => f i x) '' s) :=
  .sSup (α := αᵒᵈ) hs hf

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