norm_term_le — Mathlib

English

If ‖f n‖ ≤ ‖g n‖, then ‖term f s n‖ ≤ ‖term g s n‖.

Русский

Если ‖f(n)‖ ≤ ‖g(n)‖, то ‖term(f,s,n)‖ ≤ ‖term(g,s,n)‖.

LaTeX

$$$\\|\\operatorname{term}(f,s,n)\\| \\le \\|\\operatorname{term}(g,s,n)\\| \\quad \\text{if } \\|f(n)\\| \\le \\|g(n)\\|$$$

Lean4

theorem norm_term_le {f g : ℕ → ℂ} (s : ℂ) {n : ℕ} (h : ‖f n‖ ≤ ‖g n‖) : ‖term f s n‖ ≤ ‖term g s n‖ :=
  by
  simp only [norm_term_eq]
  split
  · rfl
  · gcongr

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