Intersection_of_Primitive_Recursive_Sets

Proved

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

computabilityprimitive-recursive-functionsproofwikiset-intersection

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

Preamble

import Mathlib.Computability.Primrec

Formal statement

theorem Intersection_of_Primitive_Recursive_Sets (f g : ℕ → ℕ) (hf : Nat.Primrec f) (hg : Nat.Primrec g) : Nat.Primrec (fun n => f n * g n) := by sorry

Source

https://proofwiki.org/wiki/Intersection_of_Primitive_Recursive_Sets

View graph