max_bi

Mathlib.Computability.AkraBazzi.SumTransform

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

Lean4

/-- Largest `b i` -/
noncomputable def max_bi (b : α → ℝ) : α :=
  Classical.choose <| Finite.exists_max b

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

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

Разделы

Аффилиация

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