not_covBy

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#not_covBy

← MathLib Explorer

English

In a densely ordered set, no pair a,b is in CovBy relation.

Русский

Во плотно упорядоченном множестве никакие две точки не образуют отношение CovBy.

LaTeX

$$$$\text{DenselyOrdered }\alpha\Rightarrow \neg(a\lessdot b).$$$$

Lean4

/-- In a dense order, nothing covers anything. -/
theorem not_covBy [DenselyOrdered α] : ¬a ⋖ b := fun h =>
  let ⟨_, hc⟩ := exists_between h.1
  h.2 hc.1 hc.2

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

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

Разделы

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

Аффилиация

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