finStronglyMeasurable_iff_measurable

English

If a family u(i,x) is continuous in i and each member is measurable in x, then the uncurry map (i,x) ↦ u(i,x) is measurable.

Русский

Если семейство функций u(i,x) непрерывно по i и измеримо по x для каждого i, то функция uncurry измерима.

LaTeX

$$$\forall x, \text{Continuous}(i \mapsto u(i,x)) \;\land\; \forall i, \text{Measurable}(u(i)) \Rightarrow \text{Measurable}(\lambda (i,x). u(i,x))$$$

Lean4

/-- In a space with second countable topology and a sigma-finite measure, `FinStronglyMeasurable`
  and `Measurable` are equivalent. -/
theorem finStronglyMeasurable_iff_measurable {_m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] :
    FinStronglyMeasurable f μ ↔ Measurable f :=
  ⟨fun h => h.measurable, fun h => (Measurable.stronglyMeasurable h).finStronglyMeasurable μ⟩

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