instIsUniversalPartialOrderTheory

Mathlib.ModelTheory.Order

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

English

For any L with IsOrdered, the partial order theory L.partialOrderTheory is universal.

Русский

Для любого L с упорядоченностью теория частичного порядка L.partialOrderTheory является универсальной.

LaTeX

$$$ \\operatorname{IsUniversal}(L.partialOrderTheory) $$$

Lean4

instance : Theory.IsUniversal L.partialOrderTheory :=
  Theory.IsUniversal.insert leSymb.isUniversal_antisymmetric

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

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

Разделы

Аффилиация

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