oneLE

Mathlib.Algebra.Order.Monoid.Submonoid

URI: https://scilib.ai/kg/mathlib#Submonoid.oneLE

← MathLib Explorer

English

oneLE M, the set of elements ≥ 1, is a submonoid of M.

Русский

oneLE M, множество элементов, не меньших 1, является подмоном M.

LaTeX

$$oneLE M$$

Lean4

/-- The submonoid of elements that are at least `1`. -/
@[to_additive (attr := simps) /-- The submonoid of nonnegative elements. -/
    ]
def oneLE : Submonoid M where
  carrier := Set.Ici 1
  mul_mem' := one_le_mul
  one_mem' := le_rfl

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

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

Разделы

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

Аффилиация

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