not_lt_zero

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.not_lt_zero

English

For every a ∈ ENNReal, a ≥ 0; in particular, ¬(a < 0).

Русский

Для каждого a ∈ ENNReal выполняется a ≥ 0; следовательно, не выполняется a < 0.

LaTeX

$$∀ a : ENNReal, a ≥ 0$$

Lean4

theorem not_lt_zero : ¬a < 0 := by simp

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

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

Разделы

Аффилиация

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