logb

Mathlib.Analysis.SpecialFunctions.Log.Base

URI: https://scilib.ai/kg/mathlib#ContinuousWithinAt.logb

English

For a finite index set and nonzero factors, log_b of the product equals the sum of log_b of factors.

Русский

Для конечного индекса и ненулевых множителей выполняется log_b(∏ f_i) = ∑ log_b(f_i).

LaTeX

$$$\log_b b (s.Prod f) = \sum i \in s, \log_b b (f i)$$$

Lean4

nonrec theorem logb (hf : ContinuousWithinAt f s a) (h₀ : f a ≠ 0) : ContinuousWithinAt (fun x => logb b (f x)) s a :=
  hf.logb h₀

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

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

Разделы

Аффилиация

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