addMonoid — Mathlib

English

The nonnegative subset carries an additive monoid structure, with addition defined componentwise and zero given by ⟨0, 0 ≥ 0⟩.

Русский

Подмножество неотрицательных элементов образует структуру аддитивного моноида: сложение определяется по компонентам, ноль—это ⟨0, 0 ≥ 0⟩.

LaTeX

$$$ (a, h_a) + (b, h_b) = (a + b, add\_nonneg h_a h_b) $$$

Lean4

instance addMonoid : AddMonoid { x : α // 0 ≤ x } :=
  Subtype.coe_injective.addMonoid _ Nonneg.coe_zero (fun _ _ => rfl) fun _ _ => rfl

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