measurable_from_prod_countable_right

English

If α is countable and measurableSingletonClass for α holds, then f : α × β → γ is measurable whenever ∀ x, y ↦ f(x,y) is measurable.

Русский

Если α счётно и выполняется условие измеримости одиночек для α, тогда f : α × β → γ измеримо, когда ∀ x, y ↦ f(x,y) измеримо.

LaTeX

$$[Countable α] [MeasurableSingletonClass α] {f : α × β → γ} (hf : ∀ x, Measurable fun y => f (x, y)) : Measurable f$$

Lean4

/-- For the version where the second space in the product is countable,
see `measurable_from_prod_countable_left`. -/
theorem measurable_from_prod_countable_right [Countable α] [MeasurableSingletonClass α] {f : α × β → γ}
    (hf : ∀ x, Measurable fun y => f (x, y)) : Measurable f :=
  measurable_from_prod_countable_right' hf (by simp +contextual)

Похожие утверждения