instCanonicallyOrderedAdd

Mathlib.Algebra.Module.Submodule.Pointwise

URI: https://scilib.ai/kg/mathlib#Submodule.instCanonicallyOrderedAdd

← MathLib Explorer

English

Submodule carries a canonical order with respect to addition.

Русский

Подмодуль несёт канонически упорядоченную по сложению структуру.

LaTeX

$$$\text{instCanonicallyOrderedAdd}(Submodule\ R\ M)$$$

Lean4

instance : CanonicallyOrderedAdd (Submodule R M)
    where
  exists_add_of_le {_a b} h := ⟨b, (sup_eq_right.2 h).symm⟩
  le_add_self _ _ := le_sup_right
  le_self_add := fun _a _b => le_sup_left

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

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

Разделы

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

Аффилиация

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