measurableSet_mutuallySingularSetSlice

English

For each a, the slice κ.mutuallySingularSetSlice η a is a measurable subset of γ.

Русский

Для каждого a срез κ.mutuallySingularSetSlice η a является измеримым подмножеством γ.

LaTeX

$$$\text{MeasurableSet}(\kappa.mutuallySingularSetSlice(\eta)(a))$$$

Lean4

theorem measurableSet_mutuallySingularSetSlice (κ η : Kernel α γ) (a : α) :
    MeasurableSet (mutuallySingularSetSlice κ η a) :=
  measurable_prodMk_left (measurableSet_mutuallySingularSet κ η)

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