oneLE_toSubmonoid

Mathlib.Algebra.Order.Group.Cone

URI: https://scilib.ai/kg/mathlib#GroupCone.oneLE_toSubmonoid

English

In the order defined by a GroupCone C, the relation a ≤ b holds if and only if b a^{-1} ∈ C.

Русский

Во порядке, заданном конусом GroupCone C, выполняется a ≤ b эквивалентно b a^{-1} ∈ C.

LaTeX

$$$(\text{mkOfGroupCone } C).le\ a\ b \iff \frac{b}{a} \in C$$$

Lean4

@[to_additive (attr := simp)]
theorem oneLE_toSubmonoid : (oneLE H).toSubmonoid = .oneLE H :=
  rfl

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

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

Разделы

Аффилиация

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