bi_min_div_two_pos

Mathlib.Computability.AkraBazzi.SumTransform

URI: https://scilib.ai/kg/mathlib#AkraBazziRecurrence.bi_min_div_two_pos

English

0 < b(min_bi b)/2; hence a positive constant exists.

Русский

0 < b(min_bi b)/2; следовательно существует положительная константа.

LaTeX

$$$0 < \dfrac{b(\min_bi b)}{2}$$$

Lean4

theorem bi_min_div_two_pos : 0 < b (min_bi b) / 2 :=
  div_pos (R.b_pos _) (by simp)

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

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

Разделы

Аффилиация

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