Union_of_Primitive_Recursive_Sets

Proved

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

computabilityprimitive-recursive-functionsproofwikiset-union

Let $A, B \subseteq \N$ be subsets of the set of natural numbers $\N$ . Let $A$ and $B$ both be primitive recursive. Then $A \cup B$ , the union of $A$ and $B$ , is primitive recursive.

Preamble

import Mathlib.Computability.Primrec

Formal statement

theorem Union_of_Primitive_Recursive_Sets (f g : ℕ → ℕ) (hf : Nat.Primrec f) (hg : Nat.Primrec g) : Nat.Primrec (fun n => if f n + g n > 0 then 1 else 0) := by sorry

Source

https://proofwiki.org/wiki/Union_of_Primitive_Recursive_Sets

View graph