lt_zero_iff

Mathlib.Data.Nat.WithBot

URI: https://scilib.ai/kg/mathlib#Nat.WithBot.lt_zero_iff

English

In WithBot ℕ, an element is below 0 exactly when it is the bottom element.

Русский

В WithBot ℕ элемент ниже нуля тогда, когда он равен ⊥.

LaTeX

$$$n < 0 \iff n = \perp$$$

Lean4

@[simp]
theorem lt_zero_iff {n : WithBot ℕ} : n < 0 ↔ n = ⊥ :=
  WithBot.lt_coe_bot

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

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

Разделы

Аффилиация

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