measurableSet_bddBelow_range — Mathlib

English

Symmetric to above: the set {b | BddBelow (range (f i b))} is measurable when each f_i is measurable and ι is countable.

Русский

Аналогично: множество {b | BddBelow (range (f i b))} измеримо при условии измеримости f_i и счетности ι.

LaTeX

$$((∀ i, Measurable (f i)) → MeasurableSet (setOf fun b => BddBelow (Set.range fun i => f i b)))$$

Lean4

theorem measurableSet_bddBelow_range {ι} [Countable ι] {f : ι → δ → α} (hf : ∀ i, Measurable (f i)) :
    MeasurableSet {b | BddBelow (range (fun i ↦ f i b))} :=
  measurableSet_bddAbove_range (α := αᵒᵈ) hf

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