linearOrderOfModels — Mathlib

English

Any model of a theory of linear orders is itself a linear order, with the order relation given by leSymb.

Русский

Любая модель теории линейных порядков сама является линейным порядком, где отношение порядка задаётся через leSymb.

LaTeX

$$$ LinearOrder M $$$

Lean4

/-- Any model of a theory of linear orders is a linear order. -/
def linearOrderOfModels [h : M ⊨ L.linearOrderTheory]
    [DecidableRel (fun (a b : M) => Structure.RelMap (leSymb : L.Relations 2) ![a, b])] : LinearOrder M
    where
  __ := L.partialOrderOfModels M
  le_total :=
    Relations.realize_total.1
      ((Theory.model_iff _).1 h _ (by simp only [linearOrderTheory, Set.mem_insert_iff, true_or]))
  toDecidableLE := inferInstance

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