English
A function f: EReal × EReal → β is measurable if its various sections on Real×Real and boundary corners are measurable.
Русский
Функция f: EReal × EReal → β измерима, если её секции на Real×Real и граничные точки измеримы.
LaTeX
$$$f: \\mathrm{EReal} \\times \\mathrm{EReal} \\to \\beta$; \\text{if } \\text{Measurable}(p \\mapsto f(p.fst.toEReal, p.snd.toEReal)) \\Rightarrow \\text{Measurable} f$ (с учётом граничных случаев)$$
Lean4
theorem measurable_of_real_real {f : EReal × EReal → β} (h_real : Measurable fun p : ℝ × ℝ ↦ f (p.1, p.2))
(h_bot_left : Measurable fun r : ℝ ↦ f (⊥, r)) (h_top_left : Measurable fun r : ℝ ↦ f (⊤, r))
(h_bot_right : Measurable fun r : ℝ ↦ f (r, ⊥)) (h_top_right : Measurable fun r : ℝ ↦ f (r, ⊤)) : Measurable f :=
by
refine measurable_of_real_prod ?_ ?_ ?_
· refine measurable_swap_iff.mp <| measurable_of_real_prod ?_ h_bot_right h_top_right
exact h_real.comp measurable_swap
· exact measurable_of_measurable_real h_bot_left
· exact measurable_of_measurable_real h_top_left
