instDefinableOfDefinable₁ — Mathlib

English

If f is definable₁ and n,g are definable as appropriate, then the function s ↦ f (g s) is definable of arity n.

Русский

Если f задаётся definable₁ и g задаётся definable на n, тогда функция s ↦ f (g s) определяется как definable на n.

LaTeX

$$$$ (f) [Definable_1 f] (n g) [Definable n g] \Rightarrow \ Definable n (\lambda s, f (g s)). $$$$

Lean4

instance (f) [Definable₁ f] (n g) [Definable n g] : Definable n (fun s ↦ f (g s)) where
  out xs := Definable₁.out f (Definable.out g xs)

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