model_dlo — Mathlib

English

If M is densely ordered and has no endpoints (no least and no greatest element), then M models the theory of dense linear orders (dlo).

Русский

Если M плотно упорядочено и в нём нет минимального или максимального элемента, то M удовлетворяет теории плотных линейных порядков (dlo).

LaTeX

$$$ M \models L.dlo $$$

Lean4

instance model_dlo [DenselyOrdered M] [NoTopOrder M] [NoBotOrder M] : M ⊨ L.dlo := by
  simp [dlo, model_linearOrder, Theory.model_insert_iff]

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