continuous_addChar_of_value_at_one

English

For r ∈ R with hr a Tendsto condition, the additive character addChar_of_value_at_one r hr: Z_p → R is continuous.

Русский

Для фиксированного r ∈ R при условии hr, равенство addChar_of_value_at_one r hr: Z_p → R является непрерывной отображением.

LaTeX

$$$$\text{Continuous}\bigl(\operatorname{addChar\_of\_value\_at\_one}(r,hr) : \mathbb{Z}_p \to R\bigr).$$$$

Lean4

@[fun_prop]
theorem continuous_addChar_of_value_at_one {r : R} (hr : Tendsto (r ^ ·) atTop (𝓝 0)) :
    Continuous (addChar_of_value_at_one r hr : ℤ_[p] → R) :=
  map_continuous (mahlerSeries (r ^ ·))

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