instCanonicallyOrderedAdd — Mathlib

English

Lie subalgebras of L form a canonically ordered additive structure under inclusion, where addition is given by the sum and the order is preserved by addition.

Русский

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

LaTeX

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

Lean4

instance : CanonicallyOrderedAdd (LieSubalgebra R L)
    where
  exists_add_of_le {_a b} h := ⟨b, (sup_eq_right.2 h).symm⟩
  le_add_self _ _ := le_sup_right
  le_self_add _ _ := le_sup_left

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