ofDigitsTerm_nonneg

Mathlib.Analysis.Real.OfDigits

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

English

Each term ofDigitsTerm is nonnegative.

Русский

Каждый член последовательности ofDigitsTerm неотрицателен.

LaTeX

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

Lean4

theorem ofDigitsTerm_nonneg {b : ℕ} {digits : ℕ → Fin b} {n : ℕ} : 0 ≤ ofDigitsTerm digits n :=
  by
  simp only [ofDigitsTerm]
  positivity

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

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

Разделы

Аффилиация

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