instModelLinearOrderTheoryOfDlo — Mathlib

English

If M satisfies dlo (dense linear order without endpoints) then M satisfies linearOrderTheory; i.e., dlo implies a linear order.

Русский

Если структура M удовлетворяет dlo (плотный линейный порядок без концов), то она удовлетворяет теории линейного порядка.

LaTeX

$$$ (M \\models L.dlo) \\Rightarrow (M \\models L.linearOrderTheory) $$$

Lean4

instance [h : M ⊨ L.dlo] : M ⊨ L.linearOrderTheory :=
  h.mono Set.subset_union_left

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