biInf — Mathlib

English

If s is countable and each f_i is measurable, the infimum over i of f_i is measurable.

Русский

Если i дискретно счетен и f_i измеримы, инфимум ∀ i∈s f_i — измерим.

LaTeX

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

Lean4

theorem biInf {ι} (s : Set ι) {f : ι → δ → α} (hs : s.Countable) (hf : ∀ i ∈ s, Measurable (f i)) :
    Measurable fun b => ⨅ i ∈ s, f i b :=
  .biSup (α := αᵒᵈ) s hs hf

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