not — Mathlib

English

Negation preserves primitive recursive predicates: if p is a primitive recursive predicate, then not p is also primitive recursive.

Русский

Отрицание примитивно вычисимого предиката также примитивно вычисимо.

LaTeX

$$$\\forall p:\\,\\alpha\\to\\mathrm{Prop},\\ PrimrecPred(p)\\to PrimrecPred(\\lambda a.\\neg p(a))$$$

Lean4

protected theorem _root_.PrimrecPred.not {p : α → Prop} : (hp : PrimrecPred p) → PrimrecPred fun a => ¬p a
  | ⟨_, hp⟩ => Primrec.primrecPred <| Primrec.not.comp hp |>.of_eq <| by simp

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