toOrderedSub — Mathlib

English

An additive group with a compatible order carries an order structure via the relation sub ≤ add.

Русский

Аддитивная группа с совместимым порядком обладает структурой упорядоченности через отношение sub ≤ add.

LaTeX

$$OrderedSub α with sub_le_iff_le_add$$

Lean4

instance (priority := 100) toOrderedSub {α : Type*} [AddGroup α] [LE α] [AddRightMono α] : OrderedSub α :=
  ⟨fun _ _ _ => sub_le_iff_le_add⟩

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