English
The norm obtained from constants is the limit of the corresponding constant-sequence; i.e., seminormFromConst' equals the limit of seminormFromConst_seq.
Русский
Норма, получаемая из констант, равна пределу соответствующей последовательности констант.
LaTeX
$$Tendsto( seminormFromConst_seq c f x) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))$$
Lean4
/-- If `x : R` is multiplicative for `f`, then it is multiplicative for
`seminormFromConst' hf1 hc hpm`. -/
theorem seminormFromConst_isMul_of_isMul {x : R} (hx : ∀ y : R, f (x * y) = f x * f y) (y : R) :
seminormFromConst' hf1 hc hpm (x * y) = seminormFromConst' hf1 hc hpm x * seminormFromConst' hf1 hc hpm y :=
have hlim :
Tendsto (seminormFromConst_seq c f (x * y)) atTop
(𝓝 (seminormFromConst' hf1 hc hpm x * seminormFromConst' hf1 hc hpm y)) :=
by
rw [seminormFromConst_apply_of_isMul hf1 hc hpm hx]
have hseq : seminormFromConst_seq c f (x * y) = fun n ↦ f x * seminormFromConst_seq c f y n :=
by
ext n
simp only [seminormFromConst_seq, mul_assoc, hx, mul_div_assoc]
simpa [hseq] using (seminormFromConst_isLimit hf1 hc hpm y).const_mul _
tendsto_nhds_unique (seminormFromConst_isLimit hf1 hc hpm (x * y)) hlim
