ofDigits_nonneg

Mathlib.Analysis.Real.OfDigits

URI: https://scilib.ai/kg/mathlib#Real.ofDigits_nonneg

← MathLib Explorer

English

The value of ofDigits is nonnegative.

Русский

Значение ofDigits неотрицательно.

LaTeX

$$$0 \le \mathrm{Real.ofDigits}( \text{digits} )$$$

Lean4

theorem ofDigits_nonneg {b : ℕ} (digits : ℕ → Fin b) : 0 ≤ ofDigits digits :=
  by
  simp only [ofDigits]
  exact tsum_nonneg fun _ ↦ ofDigitsTerm_nonneg

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

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

Разделы

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

Аффилиация

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