isGLB — Mathlib

English

The greatest lower bound of a countable family of measurable functions is measurable.

Русский

Наибольшая нижняя грань счётной семьи измеримых функций измерима.

LaTeX

$$$\text{isGLB}(f) \Rightarrow \text{Measurable}(g)$$$

Lean4

/-- If a function is the greatest lower bound of countably many measurable functions,
then it is measurable. -/
theorem isGLB {ι} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ i, Measurable (f i))
    (hg : ∀ b, IsGLB {a | ∃ i, f i b = a} (g b)) : Measurable g :=
  Measurable.isLUB (α := αᵒᵈ) hf hg

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