measurable_find — Mathlib

English

If there exists for every x a natural N with p(x,N) and each {x | p(x,k)} is measurable, then x ↦ Nat.find(p x k) is measurable.

Русский

Если для каждого x существует N such that p(x,N) и для каждого k множество {x | p(x,k)} измеримо, то x ↦ Nat.find(p x k) измеримо.

LaTeX

$$$\\forall x, \\exists N, p(x,N) \\,;\\quad \\forall k,\\ MeasurableSet\\{x \\mid p(x,k)\\}\\Rightarrow \\Measurable(x \\mapsto Nat.find(p x k))$$$

Lean4

theorem measurable_find {p : α → ℕ → Prop} [∀ x, DecidablePred (p x)] (hp : ∀ x, ∃ N, p x N)
    (hm : ∀ k, MeasurableSet {x | p x k}) : Measurable fun x => Nat.find (hp x) :=
  by
  refine measurable_to_nat fun x => ?_
  rw [preimage_find_eq_disjointed (fun k => {x | p x k})]
  exact MeasurableSet.disjointed hm _

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