instIsUniversalPreorderTheory — Mathlib

English

For any ordered language L, the preorder theory L.preorderTheory is universal.

Русский

Для любого упорядоченного языка L теория предиката порядка L.preorderTheory является универсальной.

LaTeX

$$$ \\operatorname{IsUniversal}(L.preorderTheory) $$$

Lean4

instance : Theory.IsUniversal L.preorderTheory :=
  ⟨by
    simp only [preorderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp, forall_eq]
    exact ⟨leSymb.isUniversal_reflexive, leSymb.isUniversal_transitive⟩⟩

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