English
Reiteration: a measurable supremum of countably many measurable functions is measurable.
Русский
Повторение: измеримое верхнее предел бесконечной последовательности измеримых функций измеримо.
LaTeX
$$$\forall i,\text{Measurable}(f_i) \Rightarrow \text{Measurable}(\sup_i f_i)$$$
Lean4
/-- If a function is the least upper bound of countably many measurable functions,
then it is measurable. -/
theorem isLUB {ι} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ i, Measurable (f i))
(hg : ∀ b, IsLUB {a | ∃ i, f i b = a} (g b)) : Measurable g :=
by
change ∀ b, IsLUB (range fun i => f i b) (g b) at hg
rw [‹BorelSpace α›.measurable_eq, borel_eq_generateFrom_Ioi α]
apply measurable_generateFrom
rintro _ ⟨a, rfl⟩
simp_rw [Set.preimage, mem_Ioi, lt_isLUB_iff (hg _), exists_range_iff, setOf_exists]
exact MeasurableSet.iUnion fun i => hf i (isOpen_lt' _).measurableSet
