instIsOrderedAddMonoid — Mathlib

English

The collection of Lie subalgebras of L, ordered by inclusion and with addition given by sum, forms an ordered additive monoid; in particular, addition is monotone with respect to inclusion.

Русский

Множество подалгебр Ли L, упорядоченное по включению и оснащённое операцией суммы, образует упорядоченный аддитивный моноид; сумма сохраняет порядок по включению.

LaTeX

$$$\\text{IsOrderedAddMonoid}(\\mathrm{LieSubalgebra}(R,L))$$$

Lean4

instance : IsOrderedAddMonoid (LieSubalgebra R L) where add_le_add_left _ _ := sup_le_sup_left

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