English
If each f_i is measurable and on a measurable set s you have GLB conditions, then the glued g is measurable.
Русский
Если каждый f_i измерим и на измеримом множестве s выполняются условия GLB, то склеенная g измерима.
LaTeX
$$$\forall i, \text{Measurable}(f_i) \Rightarrow \forall s, \text{MeasurableSet}(s) \Rightarrow (\forall b, IsGLB(\{a : ∃ i, f_i(b)=a\}) (g(b))) \Rightarrow \text{Measurable}(g)$$$
Lean4
/-- If a function is the greatest lower bound of countably many measurable functions on a measurable
set `s`, and coincides with a measurable function outside of `s`, then it is measurable. -/
theorem isGLB_of_mem {ι} [Countable ι] {f : ι → δ → α} {g g' : δ → α} (hf : ∀ i, Measurable (f i)) {s : Set δ}
(hs : MeasurableSet s) (hg : ∀ b ∈ s, IsGLB {a | ∃ i, f i b = a} (g b)) (hg' : EqOn g g' sᶜ)
(g'_meas : Measurable g') : Measurable g :=
Measurable.isLUB_of_mem (α := αᵒᵈ) hf hs hg hg' g'_meas
