preorderOfModels — Mathlib

English

Every model of the preorder theory carries a preorder structure, i.e. the relation interpreted as ≤ is reflexive and transitive.

Русский

Каждая модель теории предведенного порядка обладает структурой preorder; отношение ≤ рефлексивно и транзитивно.

LaTeX

$$$ \text{Preorder } M $$$

Lean4

/-- Any model of a theory of preorders is a preorder. -/
def preorderOfModels [h : M ⊨ L.preorderTheory] : Preorder M
    where
  __ := L.leOfStructure M
  le_refl :=
    Relations.realize_reflexive.1
      ((Theory.model_iff _).1 h _ (by simp only [preorderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or]))
  le_trans :=
    Relations.realize_transitive.1
      ((Theory.model_iff _).1 h _ (by simp only [preorderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, or_true]))

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