toNonneg_of_nonneg

Mathlib.Algebra.Order.Nonneg.Basic

URI: https://scilib.ai/kg/mathlib#Nonneg.toNonneg_of_nonneg

English

For any a in α, if a ≥ 0, then toNonneg a = ⟨a, a ≥ 0⟩.

Русский

Для любого a в α, если a ≥ 0, то toNonneg a = ⟨a, a ≥ 0⟩.

LaTeX

$$$ toNonneg a = \langle a, h \rangle \quad\text{при } h : 0 \le a$$$

Lean4

@[simp]
theorem toNonneg_of_nonneg {a : α} (h : 0 ≤ a) : toNonneg a = ⟨a, h⟩ := by simp [toNonneg, h]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru