English
Let f be a ring seminorm on a commutative ring R, and fix c ∈ R with f(1) ≤ 1 and f(c) ≠ 0, together with a pow-multiplicativity property IsPowMul. Then the evaluation of the constant-based seminorm at c coincides with f(c): seminormFromConst'(hf1 hc hpm)(c) = f(c).
Русский
Пусть f является кольцевой сепинормой на коммутативном кольце R, зафиксируем c ∈ R с f(1) ≤ 1 и f(c) ≠ 0, а также свойство IsPowMul. Тогда значение семинормы от константы в точке c равно f(c): seminormFromConst'(hf1 hc hpm)(c) = f(c).
LaTeX
$$$\operatorname{seminormFromConst'}_{hf1,hc,hpm}(c) = f(c)$$$
Lean4
/-- `seminormFromConst' hf1 hc hpm c = f c`. -/
theorem seminormFromConst_apply_c : seminormFromConst' hf1 hc hpm c = f c :=
have hlim : Tendsto (seminormFromConst_seq c f c) atTop (𝓝 (f c)) :=
by
have hseq : seminormFromConst_seq c f c = fun _n ↦ f c :=
by
ext n
simp only [seminormFromConst_seq]
rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm, mul_div_assoc, div_self (pow_ne_zero n hc),
mul_one]
rw [hseq]
exact tendsto_const_nhds
tendsto_nhds_unique (seminormFromConst_isLimit hf1 hc hpm c) hlim
