measurable_uniqueElim_cylinderEvents

English

If the index type ι has a unique element, then the canonical elimination function uniqueElim: X(default) → ∀ i, X(i) is measurable.

Русский

Если индексы образуют единичное множество, то функция uniqueElim: X(default) → ∀ i, X(i) измерима.

LaTeX

$$$\\text{measurable\\_uniqueElim\\_cylinderEvents} \\ : \\ Measurable(uniqueElim : X(\\text{default}) \\to \\forall i, X(i))$$$

Lean4

theorem measurable_uniqueElim_cylinderEvents [Unique ι] : Measurable (uniqueElim : X (default : ι) → ∀ i, X i) := by
  simp_rw [measurable_pi_iff, Unique.forall_iff, uniqueElim_default]; exact measurable_id

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