add — Mathlib

English

There is an addition operation on the nonnegative subtype, making it an additive structure.

Русский

На подпредмете неотрицательных элементов есть операция сложения, образующая аддитивную структуру.

LaTeX

$$$Nonneg.add$ defines an addition on { x : α // 0 ≤ x } by (⟨x, hx⟩, ⟨y, hy⟩) ↦ ⟨x+y, add\_nonneg hx hy⟩$$

Lean4

instance add [AddZeroClass α] [Preorder α] [AddLeftMono α] : Add { x : α // 0 ≤ x } :=
  ⟨fun x y => ⟨x + y, add_nonneg x.2 y.2⟩⟩

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