nonneg

Mathlib.Topology.UnitInterval

URI: https://scilib.ai/kg/mathlib#unitInterval.nonneg

English

For x ∈ I, 0 ≤ x (as a real number).

Русский

Для x ∈ I верно: x ≥ 0 (как число на прямой).

LaTeX

$$$\\forall x\\in I,\\ 0 \\le x$$$

Lean4

theorem nonneg (x : I) : 0 ≤ (x : ℝ) :=
  x.2.1

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

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

Разделы

Аффилиация

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