instIsLeftCancelAddSubtypeLeOfNat

English

If addition is left-cancellable in α, it remains left-cancellable in the nonnegative subtype.

Русский

Если сложение слева в α отменяемо, то это свойство сохраняется и в подпредмете.

LaTeX

$$Instance IsLeftCancelAdd for { x : α // 0 ≤ x }$$

Lean4

instance [AddZeroClass α] [Preorder α] [AddLeftMono α] [IsLeftCancelAdd α] : IsLeftCancelAdd { x : α // 0 ≤ x } where
  add_left_cancel _ _ _ eq := Subtype.ext (add_left_cancel congr($eq))

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