measurable_findGreatest' — Mathlib

English

If p: α → Nat → Prop is decidable and for each k ≤ N the set {x | p(x,N) = k} is measurable, then x ↦ Nat.findGreatest(p x) N is measurable.

Русский

Если p: α → Nat → Prop.Decidable и для каждого k ≤ N множество {x | p(x,N) = k} измеримо, то x ↦ Nat.findGreatest(p x) N измеримо.

LaTeX

$$$\\forall (p: α \\to Nat \\to Prop)\\ [DecidablePred p] \\{N : Nat\\},\\ (\\forall k \\le N,\\ MeasurableSet\\{x \\mid Nat.findGreatest(p x) N = k\\}) \\Rightarrow \\text{Measurable } x \\mapsto Nat.findGreatest(p x) N$$$

Lean4

theorem measurable_findGreatest' {p : α → ℕ → Prop} [∀ x, DecidablePred (p x)] {N : ℕ}
    (hN : ∀ k ≤ N, MeasurableSet {x | Nat.findGreatest (p x) N = k}) : Measurable fun x => Nat.findGreatest (p x) N :=
  measurable_to_nat fun _ => hN _ N.findGreatest_le

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