not — Mathlib

English

The negation of a computable predicate is computable, given the predicate itself is computable.

Русский

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

LaTeX

$$ComputablePred p → ComputablePred (fun a => ¬ p a)$$

Lean4

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

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