cast_nonpos

Mathlib.Data.Nat.Cast.Order.Basic

URI: https://scilib.ai/kg/mathlib#Nat.cast_nonpos

English

For all n, (n : α) ≤ 0 iff n = 0.

Русский

Для всех n, (n : α) ≤ 0 эквивалентно n = 0.

LaTeX

$$$\forall n \in \mathbb{N},\ (n : \alpha) \le 0 \iff n = 0.$$$

Lean4

@[simp]
theorem cast_nonpos : (n : α) ≤ 0 ↔ n = 0 := by norm_cast; cutsat

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

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

Разделы

Аффилиация

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