pair — Mathlib

English

If f,g are computable, then a ↦ (f a, g a) is computable.

Русский

Если f и g вычислимы, то функция a ↦ (f a, g a) вычислима.

LaTeX

$$$\text{Computable } f \to \text{Computable } g \to \text{Computable } (\lambda a. (f a, g a))$$$

Lean4

nonrec theorem pair {f : α → β} {g : α → γ} (hf : Computable f) (hg : Computable g) : Computable fun a => (f a, g a) :=
  (hf.pair hg).of_eq fun n => by cases decode (α := α) n <;> simp [Seq.seq]

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