English
Let α be countable. If for each x, y ↦ f(x,y) is measurable and if f respects a compatibility condition across x' in measurableAtom x, then f is measurable.
Русский
Пусть α счётно. Если для каждого x функция y ↦ f(x,y) измерима и если f удовлетворяет совместимости по x' внутри измеримой атомы x, тогда f измерима.
LaTeX
$$$[Countable \ α] \; {f : \alpha \times β \to γ}\; (hf : \forall x, \operatorname{Measurable}(y \mapsto f(x,y))) \\ (h'f : \forall x\, x'\, y, x' \in \operatorname{measurableAtom}(x) \to f(x',y) = f(x,y)) \Rightarrow \operatorname{Measurable} f$$$
Lean4
/-- See `measurable_from_prod_countable_right` for a version where we assume that singletons are
measurable instead of reasoning about `measurableAtom`. -/
theorem measurable_from_prod_countable_right' [Countable α] {f : α × β → γ} (hf : ∀ x, Measurable fun y => f (x, y))
(h'f : ∀ x x' y, x' ∈ measurableAtom x → f (x', y) = f (x, y)) : Measurable f :=
by
change Measurable ((fun p ↦ f (p.2, p.1)) ∘ Prod.swap)
exact (measurable_from_prod_countable_left' hf h'f).comp measurable_swap
