exists — Mathlib

English

Let ι be countable and p_i: α → Prop with each p_i measurable. Then a ↦ ∃ i, p_i(a) is measurable.

Русский

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

LaTeX

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

Lean4

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

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