measurable_pi_apply — Mathlib

English

For fixed a, the evaluation map is measurable: the map f ↦ f(a) is measurable from the space of α-valued functions to X(a).

Русский

Для фиксированного индекса a отображение оценки измеримо: отображение f ↦ f(a) есть измеримо из пространства функций в X(a).

LaTeX

$$$\text{Measurable}(f \mapsto f(a))$ for fixed a, i.e. Measurable(\lambda f: \forall a, X(a). f(a))$$

Lean4

@[fun_prop, aesop safe 100 apply (rule_sets := [Measurable])]
theorem measurable_pi_apply (a : δ) : Measurable fun f : ∀ a, X a => f a :=
  measurable_pi_iff.1 measurable_id a

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