measurable_update_cylinderEvents — Mathlib

English

In a singleton index, universal quantification reduces to evaluation at the unique element; this yields simple equalities used in proofs about uniqueElim.

Русский

В единичном множестве индексов всеобщая квантификация сводится к оценке в уникальном элементе, что дает простые тождества для uniqueElim.

LaTeX

$$$\\forall p:\\; (∀ a, p(a)) = p(u)\\text{ where } u = Unique.instInhabited.default$$$

Lean4

/-- The function `update f a : X a → Π a, X a` is always measurable.
This doesn't require `f` to be measurable.
This should not be confused with the statement that `update f a x` is measurable. -/
@[measurability]
theorem measurable_update_cylinderEvents (f : ∀ a : ι, X a) {a : ι} [DecidableEq ι] :
    @Measurable _ _ _ (cylinderEvents Δ) (update f a) :=
  measurable_update_cylinderEvents'.comp measurable_prodMk_left

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