instModelPreorderTheoryOfPartialOrderTheory

Mathlib.ModelTheory.Order

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

English

If a structure M is ordered, then the order relation maps to an expanded structure, i.e., LHom.IsExpansionOn (orderLHom L) M.

Русский

Если структура M упорядочена, то отображение порядка расширяет структуру: LHom.IsExpansionOn (orderLHom L) M.

LaTeX

$$$ LHom.IsExpansionOn (orderLHom L) M $$$

Lean4

instance [h : M ⊨ L.partialOrderTheory] : M ⊨ L.preorderTheory :=
  h.mono (Set.subset_insert _ _)

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

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

Разделы

Аффилиация

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