forall — Mathlib

English

Let ι be countable and p_i: α → Prop be a family of predicates such that each p_i is measurable. Then the predicate a ↦ ∀ i, p_i(a) is measurable.

Русский

Пусть ι счётно, и для каждого i; p_i: α → Prop измерим. Тогда a ↦ ∀ i, p_i(a) измерим.

LaTeX

$$$[\text{Countable } \iota] \; (\forall i, \mathrm{Measurable}(p_i)) \Rightarrow \mathrm{Measurable}(a \mapsto \forall i, p_i(a))$$$

Lean4

theorem «forall» [Countable ι] {p : ι → α → Prop} (hp : ∀ i, Measurable (p i)) : Measurable fun a ↦ ∀ i, p i a :=
  measurableSet_setOf.1 <| by rw [setOf_forall]; exact MeasurableSet.iInter fun i ↦ (hp i).setOf

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