and — Mathlib

English

If p and q are primitive recursive predicates, then their conjunction is primitive recursive.

Русский

Если предикаты p и q примитивно вычисимы, то их конъюнкция тоже примитивно вычисима.

LaTeX

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

Lean4

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

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