English
Let β be countable. If for each y, x ↦ f(x,y) is measurable and if f satisfies a compatibility condition across y' in measurableAtom y, then f is measurable.
Русский
Пусть β счётно. Если для каждого y функция x ↦ f(x,y) измерима и если f удовлетворяет совместимости по y' внутри измеримой мины y, тогда f измерима.
LaTeX
$$$[Countable\, \beta] \; {f : \alpha \times \beta \to \gamma}\; (hf : \forall y, \operatorname{Measurable}(x \mapsto f(x,y))) \\ (h'f : \forall y\, y'\, x,\ y' \in \operatorname{measurableAtom}(y) \to f(x,y') = f(x,y)) \Rightarrow \operatorname{Measurable} f$$$
Lean4
/-- See `measurable_from_prod_countable_left` for a version where we assume that singletons are
measurable instead of reasoning about `measurableAtom`. -/
theorem measurable_from_prod_countable_left' [Countable β] {f : α × β → γ} (hf : ∀ y, Measurable fun x => f (x, y))
(h'f : ∀ y y' x, y' ∈ measurableAtom y → f (x, y') = f (x, y)) : Measurable f := fun s hs =>
by
have : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ (measurableAtom y : Set β) :=
by
ext1 ⟨x, y⟩
simp only [mem_preimage, mem_iUnion, mem_prod]
refine ⟨fun h ↦ ⟨y, h, mem_measurableAtom_self y⟩, ?_⟩
rintro ⟨y', hy's, hy'⟩
rwa [h'f y' y x hy']
rw [this]
exact .iUnion (fun y ↦ (hf y hs).prod (.measurableAtom_of_countable y))
