eval — Mathlib

English

If g is measurable, then for any fixed a, the map x ↦ g x a is measurable.

Русский

Если g измеримо, то для любого фиксированного a отображение x ↦ g(x)(a) измеримо.

LaTeX

$$$\operatorname{Measurable} g \rightarrow \operatorname{Measurable}(\lambda x. g x a)$$$

Lean4

@[aesop safe 100 apply (rule_sets := [Measurable])]
theorem eval {a : δ} {g : α → ∀ a, X a} (hg : Measurable g) : Measurable fun x => g x a :=
  (measurable_pi_apply a).comp hg

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