instDenselyOrderedUnits

Mathlib.Algebra.Order.GroupWithZero.Canonical

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

English

If α is densely ordered, then αˣ is densely ordered.

Русский

Если α плотно упорядочено, то αˣ плотно упорядочено.

LaTeX

$$$DenselyOrdered \\\\alpha \\\\Rightarrow DenselyOrdered \\\\alpha^{\\\\times}$$$

Lean4

instance [DenselyOrdered α] : DenselyOrdered αˣ :=
  have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
  by tauto

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

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

Разделы

Аффилиация

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