model_partialOrder — Mathlib

English

If M has a partial order and L.OrderedStructure M, then M models L.partialOrderTheory.

Русский

Если M имеет частичный порядок и L.OrderedStructure M, то M удовлетворяет L.partialOrderTheory.

LaTeX

$$$ (PartialOrder\\toPreorder) \\Rightarrow M \\models L.partialOrderTheory $$$

Lean4

instance model_partialOrder [PartialOrder M] [L.OrderedStructure M] : M ⊨ L.partialOrderTheory :=
  by
  simp only [partialOrderTheory, Theory.model_insert_iff, Relations.realize_antisymmetric, relMap_leSymb, Fin.isValue,
    Matrix.cons_val_zero, Matrix.cons_val_one, model_preorder, and_true]
  exact fun _ _ => le_antisymm

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