logCounting_eval_zero — Mathlib

English

The logarithmic counting function evaluated at zero is zero: logCounting D 0 = 0 for any locally finite D.

Русский

Логарифмическая функция подсчета в нуле равна нулю: logCounting D 0 = 0 для любой локально ограниченной D.

LaTeX

$$$\logCounting(D)(0) = 0$$$

Lean4

/-- Evaluation of the logarithmic counting function at zero yields zero.
-/
@[simp]
theorem logCounting_eval_zero {E : Type*} [NormedAddCommGroup E] [ProperSpace E]
    (D : locallyFinsuppWithin (univ : Set E) ℤ) : logCounting D 0 = 0 := by simp [logCounting]

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