English
If each coordinate space α_i carries a measurable division, then the space of functions ∀ i, α_i carries a measurable division; equivalently, coordinatewise division of two functions is measurable.
Русский
Если у каждого пространства координат α_i есть измеримое деление, то пространство функций ∀ i, α_i также имеет измеримое деление; иначе говоря, по координатами деление двух функций измеримо.
LaTeX
$$$\\text{MeasurableDiv}((i: ι) \\to (α_i))$$$
Lean4
@[to_additive]
instance measurableDiv {ι : Type*} {α : ι → Type*} [∀ i, Div (α i)] [∀ i, MeasurableSpace (α i)]
[∀ i, MeasurableDiv (α i)] : MeasurableDiv (∀ i, α i) :=
⟨fun _ => measurable_pi_iff.mpr fun i => (measurable_pi_apply i).const_div _, fun _ =>
measurable_pi_iff.mpr fun i => (measurable_pi_apply i).div_const _⟩
