denselyOrdered_of_dlo

Mathlib.ModelTheory.Order

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.denselyOrdered_of_dlo

← MathLib Explorer

English

If dlo holds in M, then M is densely ordered.

Русский

Если в M выполняется dlo, то M плотно упорядочено.

LaTeX

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

Lean4

theorem denselyOrdered_of_dlo [M ⊨ L.dlo] : DenselyOrdered M :=
  realize_denselyOrdered_iff.1
    (L.dlo.realize_sentence_of_mem
      (by simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or, or_true]))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru