English
A function f: EReal × β → γ is measurable if its restriction to Real×β is measurable and its values at (⊥,·) and (⊤,·) are measurable (and similarly for other boundary cases).
Русский
Функция f: EReal × β → γ измерима, если её ограничение на Real×β измеримо, и значения на (⊥,·) и (⊤,·) измеримы (а также другие граничные случаи).
LaTeX
$$$f: \\mathrm{EReal} \\times \\beta \\to \\gamma$; \\text{ if } f\\text{ is measurable when fst := toEReal and snd varying, and at }(⊥,·),(⊤,·) \\text{, then } f \\text{ is measurable}$$$
Lean4
theorem measurable_of_real_prod {f : EReal × β → γ} (h_real : Measurable fun p : ℝ × β ↦ f (p.1, p.2))
(h_bot : Measurable fun x ↦ f (⊥, x)) (h_top : Measurable fun x ↦ f (⊤, x)) : Measurable f :=
.of_union₃_range_cover (measurableEmbedding_prodMk_left _) (measurableEmbedding_prodMk_left _)
(measurableEmbedding_coe.prodMap .id) (by simp [-univ_subset_iff, subset_def, EReal.forall]) h_bot h_top h_real
