isAlgebraic_sum

Mathlib.ModelTheory.Basic

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

English

If L and L' are algebraic languages, their sum is algebraic.

Русский

Если L и L' являются алгебраическими языками, их сумма алгебраическая.

LaTeX

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

Lean4

instance isAlgebraic_sum [L.IsAlgebraic] [L'.IsAlgebraic] : IsAlgebraic (L.sum L') := fun _ => instIsEmptySum

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

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

Разделы

Аффилиация

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