nonneg_iff_ne_neg_one

Mathlib.Data.Sign.Defs

URI: https://scilib.ai/kg/mathlib#SignType.nonneg_iff_ne_neg_one

English

For a ∈ SignType, 0 ≤ a if and only if a ≠ -1.

Русский

Для a ∈ SignType, 0 ≤ a если и только если a ≠ -1.

LaTeX

$$$0 \le a \iff a \neq -1$$$

Lean4

theorem nonneg_iff_ne_neg_one {a : SignType} : 0 ≤ a ↔ a ≠ -1 := by decide +revert

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

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

Разделы

Аффилиация

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