measurable_uniqueElim — Mathlib

English

If δ has a unique element, the evaluation of the uniqueElim function is measurable.

Русский

Если в пространстве есть уникальный элемент, то функция uniqueElim измерима.

LaTeX

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

Lean4

@[measurability, fun_prop]
theorem measurable_uniqueElim [Unique δ] : Measurable (uniqueElim : X (default : δ) → ∀ i, X i) := by
  simp_rw [measurable_pi_iff, Unique.forall_iff, uniqueElim_default]; exact measurable_id

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