measurable_from_prod_countable_left

English

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

Русский

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

LaTeX

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

Lean4

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

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