pow

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsEquivalent.pow

← MathLib Explorer

English

If t ~_l u, then t^n ~_l u^n for every natural n.

Русский

Если t ~_l u, то t^n ~_l u^n для любого натурального n.

LaTeX

$$$ (t \\sim_{l} u) \\Rightarrow \\forall n,\\ t^n \\sim_{l} u^n $$$

Lean4

protected theorem pow (h : t ~[l] u) (n : ℕ) : t ^ n ~[l] u ^ n := by
  induction n with
  | zero => simpa using IsEquivalent.refl
  | succ _ ih => simpa [pow_succ] using ih.mul h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru