one

Mathlib.Algebra.Order.Nonneg.Basic

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

Lean4

instance one : One { x : α // 0 ≤ x } where one := ⟨1, zero_le_one⟩

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

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

Разделы

Аффилиация

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