measurable_findGreatest — Mathlib

English

If for each k ≤ N the set {x | p(x,k)} is measurable, then x ↦ Nat.findGreatest(p x,k) is measurable.

Русский

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

LaTeX

$$$\\forall k \\le N,\\ MeasurableSet\\{x \\mid p(x,k)\\}$ implies Measurable x \\mapsto Nat.findGreatest(p x) N$$

Lean4

theorem measurable_findGreatest {p : α → ℕ → Prop} [∀ x, DecidablePred (p x)] {N}
    (hN : ∀ k ≤ N, MeasurableSet {x | p x k}) : Measurable fun x => Nat.findGreatest (p x) N :=
  by
  refine measurable_findGreatest' fun k hk => ?_
  simp only [Nat.findGreatest_eq_iff, setOf_and, setOf_forall, ← compl_setOf]
  repeat'
    apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.compl, hN] <;> try intros

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