instLocallyFiniteOrderUnits

Mathlib.GroupTheory.ArchimedeanDensely

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

← MathLib Explorer

English

If X is a locally finite ordered structure, then the units of X inherit a locally finite order from X.

Русский

Единицы X наследуют локально конечный порядок от X.

LaTeX

$$$\text{LocallyFiniteOrder}(\mathrm{Units}(X))$$$

Lean4

noncomputable instance [Monoid X] : LocallyFiniteOrder (Units X) :=
  OrderEmbedding.locallyFiniteOrder (⟨⟨Units.val, Units.val_injective⟩, by simp⟩ : Units X ↪o X)

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

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

Разделы

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

Аффилиация

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