model_linearOrder — Mathlib

English

Let L be an ordered language and M a structure whose universe is linearly ordered in a way compatible with L. Then M satisfies the axioms of a linear order, i.e. M is a model of L.linearOrderTheory.

Русский

Пусть L — упорядоченный язык, а M — структура с линейно упорядованной областью определения, совместимой с L. Тогда M удовлетворяет аксиомам линейного порядка, то есть M является моделью L.linearOrderTheory.

LaTeX

$$$ M \models L.linearOrderTheory $$$

Lean4

instance model_linearOrder : M ⊨ L.linearOrderTheory :=
  by
  simp only [linearOrderTheory, Theory.model_insert_iff, Relations.realize_total, relMap_leSymb, Fin.isValue,
    Matrix.cons_val_zero, Matrix.cons_val_one, model_partialOrder, and_true]
  exact le_total

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