truncateToReal_nonneg

Mathlib.Topology.Instances.ENNReal.Lemmas

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

English

The truncated real value is always nonnegative: 0 ≤ truncateToReal t x.

Русский

Сокращённое значение неотрицательное: 0 ≤ truncateToReal t x.

LaTeX

$$$0 \leq \text{truncateToReal}(t, x)$$$

Lean4

theorem truncateToReal_nonneg {t x : ℝ≥0∞} : 0 ≤ truncateToReal t x :=
  toReal_nonneg

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

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

Разделы

Аффилиация

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