instDefinableOfDefinable₂ — Mathlib

English

If f is definable₂ and g1,g2 are definable on n, then s ↦ f (g1 s) (g2 s) is definable on n.

Русский

Если f задаётся definable₂ и g1,g2 задаются definable на n, то s ↦ f (g1 s) (g2 s) тоже definable на n.

LaTeX

$$$$ (f) [Definable_2 f] (n g_1 g_2) [Definable n g_1] [Definable n g_2] \Rightarrow \ Definable n (\lambda s, f (g_1 s) (g_2 s)). $$$$

Lean4

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

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