zero — Mathlib

English

There is a canonical zero element in the nonnegative subtype, given by ⟨0, 0 ≤ 0⟩, serving as the zero for addition.

Русский

Существует канонический ноль в подпредмете неотрицательных элементов: ⟨0, 0 ≤ 0⟩, который является нулём относительно сложения.

LaTeX

$$$Zero \\{ x : α // 0 ≤ x \\} = ⟨0, le_rfl⟩$$$

Lean4

instance zero [Zero α] [Preorder α] : Zero { x : α // 0 ≤ x } :=
  ⟨⟨0, le_rfl⟩⟩

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