noBotOrder_of_dlo

Mathlib.ModelTheory.Order

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

← MathLib Explorer

English

From dlo, deduce NoTopOrder; same idea as 148143 but framed differently.

Русский

Из dlo следует NoTopOrder; формулировка дубликата.

LaTeX

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

Lean4

theorem noBotOrder_of_dlo [M ⊨ L.dlo] : NoBotOrder M :=
  realize_noBotOrder_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