cast_le_neg_one_or_one_le_cast_of_ne_zero

Mathlib.Algebra.Order.Ring.Cast

URI: https://scilib.ai/kg/mathlib#Int.cast_le_neg_one_or_one_le_cast_of_ne_zero

← MathLib Explorer

English

For any integer n ≠ 0, either n.cast ≤ −1 or 1 ≤ n.cast.

Русский

Для любого n ≠ 0 либо n.cast ≤ −1, либо 1 ≤ n.cast.

LaTeX

$$n^{\mathsf{cast}} \le -1 \;\lor\; 1 \le n^{\mathsf{cast}}$$

Lean4

theorem cast_le_neg_one_or_one_le_cast_of_ne_zero (hn : n ≠ 0) : (n : R) ≤ -1 ∨ 1 ≤ (n : R) :=
  hn.lt_or_gt.imp cast_le_neg_one_of_neg cast_one_le_of_pos

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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