isRelational_sum

Mathlib.ModelTheory.Basic

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.isRelational_sum

English

If L and L' are relational languages, then their sum is a relational language.

Русский

Если L и L' являются языками с отношениями, их сумма является языком с отношениями.

LaTeX

$$$[L.IsRelational] \; [L'.IsRelational] \Rightarrow (L.sum L').IsRelational$$$

Lean4

instance isRelational_sum [L.IsRelational] [L'.IsRelational] : IsRelational (L.sum L') := fun _ => instIsEmptySum

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru