isRelational_constantsOn — Mathlib

English

If α is empty, the language constantsOn α contains only relation symbols (no function symbols).

Русский

Если α пуст, язык constantsOn α состоит только из реляционных символов (нет функциональных).

LaTeX

$$$\\operatorname{IsEmpty}(\\alpha) \\Rightarrow (constantsOn \\alpha).IsRelational$$$

Lean4

instance isRelational_constantsOn [_ie : IsEmpty α] : IsRelational (constantsOn α) := fun n =>
  Nat.casesOn n _ie inferInstance

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