toNonneg_le

Mathlib.Algebra.Order.Nonneg.Basic

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

English

The order on α is reflected by toNonneg: toNonneg a ≤ b iff a ≤ b.

Русский

Порядок на α отражается в toNonneg: toNonneg a ≤ b ⇔ a ≤ b.

LaTeX

$$$ toNonneg a \le b \iff a \le b $$$

Lean4

@[simp]
theorem toNonneg_le {a : α} {b : { x : α // 0 ≤ x }} : toNonneg a ≤ b ↔ a ≤ b :=
  by
  obtain ⟨b, hb⟩ := b
  simp [toNonneg, hb]

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

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

Разделы

Аффилиация

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