imp — Mathlib

English

If p and q are measurable predicates on α, then the implication p → q is measurable as a predicate.

Русский

Если p и q — измеримые предикаты, то импликация p → q измерима как предикат.

LaTeX

$$$\mathrm{Measurable}(p) \land \mathrm{Measurable}(q) \Rightarrow \mathrm{Measurable}(\lambda a. p(a) \rightarrow q(a))$$$

Lean4

theorem imp (hp : Measurable p) (hq : Measurable q) : Measurable fun a ↦ p a → q a :=
  measurableSet_setOf.1 <| hp.setOf.himp hq.setOf

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