seminormFromConst_seq_zero — Mathlib

English

If f(0) = 0, then seminormFromConst_seq c f 0 = 0; the sequence at 0 is identically zero.

Русский

Если f(0)=0, то seminormFromConst_seq c f 0 = 0; последовательность в нуле тождественно ноль.

LaTeX

$$$f(0)=0 \Rightarrow seminormFromConst_seq\ c\ f\ 0 = 0$$$

Lean4

/-- `seminormFromConst_seq c f 0` is the constant sequence zero. -/
theorem seminormFromConst_seq_zero (hf : f 0 = 0) : seminormFromConst_seq c f 0 = 0 :=
  by
  rw [seminormFromConst_seq_def]
  ext n
  rw [zero_mul, hf, zero_div, Pi.zero_apply]

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