or — Mathlib · SciLib

English

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

Русский

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

LaTeX

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

Lean4

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

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