Complement_of_Primitive_Recursive_Set

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

computabilityprimitive-recursive-functionsproofwikirelative-complement

Let $S \subseteq \N$ be primitive recursive. Then its relative complement $\N \setminus S$ of $S$ in $\N$ is primitive recursive.

Preamble

import Mathlib.Computability.Primrec

Formal statement

theorem Complement_of_Primitive_Recursive_Set (S : Set ℕ) (hS : ∀ n, Decidable (n ∈ S)) (hPR : Nat.Primrec (fun n => if n ∈ S then 1 else 0)) : Nat.Primrec (fun n => if n ∈ S then 0 else 1) := by sorry

Source

https://proofwiki.org/wiki/Complement_of_Primitive_Recursive_Set

View graph