isEmpty_functions_constantsOn_succ

English

In the language that consists only of constants from α, there are no function symbols of arity n+1 for any n.

Русский

Язык, состоящий только из констант α, не имеет констант-символов функций произвольной положительной арности.

LaTeX

$$$ #\\bigl((constantsOn \\alpha).Functions (n+1)\\bigr) = 0 $$$

Lean4

instance isEmpty_functions_constantsOn_succ {n : ℕ} : IsEmpty ((constantsOn α).Functions (n + 1)) :=
  inferInstanceAs (IsEmpty PEmpty)

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