partialOrderOfModels

Mathlib.ModelTheory.Order

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

Lean4

/-- Any model of a theory of partial orders is a partial order. -/
def partialOrderOfModels [h : M ⊨ L.partialOrderTheory] : PartialOrder M
    where
  __ := L.preorderOfModels M
  le_antisymm :=
    Relations.realize_antisymmetric.1
      ((Theory.model_iff _).1 h _ (by simp only [partialOrderTheory, Set.mem_insert_iff, true_or]))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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