denselyOrdered_units_iff

Mathlib.Algebra.Order.GroupWithZero.Canonical

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

← MathLib Explorer

English

Densely ordered units α is equivalent to densely ordered α.

Русский

Плотно упорядоченные единицы α эквивалентны плотной структуре α.

LaTeX

$$$DenselyOrdered (Units α) \\\\Leftrightarrow DenselyOrdered α$$$

Lean4

theorem denselyOrdered_units_iff [Nontrivial αˣ] : DenselyOrdered αˣ ↔ DenselyOrdered α :=
  have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
  by tauto

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

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

Разделы

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

Аффилиация

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