measurableDiv₂ — Mathlib

English

If each coordinate α_i has a measurable division, then the pointwise division of two functions on the product space is measurable, i.e., the map (f,g) ↦ (i ↦ f(i)/g(i)) is measurable.

Русский

Если каждый компонент α_i имеет измеримое деление, то пообразование деления двух функций на произведении координат измеримо: (f,g) ↦ (i ↦ f(i)/g(i)).

LaTeX

$$$\\text{MeasurableDiv₂}((i: ι) \\to α_i)$$$

Lean4

@[to_additive Pi.measurableSub₂]
instance measurableDiv₂ {ι : Type*} {α : ι → Type*} [∀ i, Div (α i)] [∀ i, MeasurableSpace (α i)]
    [∀ i, MeasurableDiv₂ (α i)] : MeasurableDiv₂ (∀ i, α i) :=
  ⟨measurable_pi_iff.mpr fun _ => measurable_fst.eval.div measurable_snd.eval⟩

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