model_preorder — Mathlib

English

In a model of an ordered language, the preorder theory holds.

Русский

В модели упорядоченного языка выполняется теория предиката порядка.

LaTeX

$$$ M \\models L.preorderTheory $$$

Lean4

instance model_preorder : M ⊨ L.preorderTheory :=
  by
  simp only [preorderTheory, Theory.model_insert_iff, Relations.realize_reflexive, relMap_leSymb,
    Theory.model_singleton_iff, Relations.realize_transitive]
  exact ⟨le_refl, fun _ _ _ => le_trans⟩

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