not_denselyOrdered

Mathlib.GroupTheory.ArchimedeanDensely

URI: https://scilib.ai/kg/mathlib#Int.not_denselyOrdered

English

The integers are not densely ordered: between 0 and 1 there is no integer.

Русский

Целые числа не плотны: между 0 и 1 нет целого числа.

LaTeX

$$$\lnot\mathrm{DenselyOrdered}(\mathbb{Z})$$$

Lean4

theorem not_denselyOrdered : ¬DenselyOrdered ℤ :=
  (LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered ℤ).mp ⟨.refl _⟩

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

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

Разделы

Аффилиация

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