pow — Mathlib

English

If f = o_l g, then for every n ≥ 1, the n-th power of f is o_l the n-th power of g.

Русский

Если f = o_l g, то для каждого n ≥ 1 выполняется f^n = o_l g^n.

LaTeX

$$$f =o_l g \\Rightarrow \\forall n \\in \\mathbb{N},\\ n>0:\\ f^n =o_l g^n.$$$

Lean4

theorem pow {f : α → R} {g : α → S} (h : f =o[l] g) {n : ℕ} (hn : 0 < n) : (fun x => f x ^ n) =o[l] fun x => g x ^ n :=
  by
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'; clear hn
  induction n with
  | zero => simpa only [pow_one]
  | succ n ihn => convert ihn.mul h <;> simp [pow_succ]

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