part_iff — Mathlib

English

For every natural number n and every function f represented as a partial function on n-length vectors of natural numbers, the n-ary partial recursive predicate Partrec' f holds if and only if the standard Partrec predicate holds for f.

Русский

Для каждого натурального числа n и для каждой функции f, заданной как частичная функция на векторах из n натуральных чисел, выполняется эквивалентность: Partrec' f ⇔ Partrec f.

LaTeX

$$$ \forall n, f,\; @Partrec' n f \iff _root_.Partrec f $$$

Lean4

theorem part_iff {n f} : @Partrec' n f ↔ _root_.Partrec f :=
  ⟨to_part, of_part⟩

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