sqrt

Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsTheta.sqrt

← MathLib Explorer

English

If f = Θ_l g, then sqrt f = Θ_l sqrt g.

Русский

Если f = Θ_l g, тогда sqrt f = Θ_l sqrt g.

LaTeX

$$$$ \sqrt{f} = Θ_l (\sqrt{g}) $$$$

Lean4

protected theorem sqrt (hfg : f =Θ[l] g) (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) :
    (Real.sqrt <| f ·) =Θ[l] (Real.sqrt <| g ·) :=
  ⟨hfg.1.sqrt hg, hfg.2.sqrt hf⟩

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

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

Разделы

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

Аффилиация

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