sup

Mathlib.Analysis.Asymptotics.Theta

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

English

If f' =Θ_l g' and f' =Θ_l' g' then f' =Θ_{l ⊔ l'} g'.

Русский

Если f' =Θ_l g' и f' =Θ_l' g', тогда f' =Θ_{l ⊔ l'} g'.

LaTeX

$$$ (f' =\Theta_{l} g') \land (f' =\Theta_{l'} g') \Rightarrow f' =\Theta_{l \sqcup l'} g'. $$$

Lean4

theorem sup (h : f' =Θ[l] g') (h' : f' =Θ[l'] g') : f' =Θ[l ⊔ l'] g' :=
  ⟨h.1.sup h'.1, h.2.sup h'.2⟩

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

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

Разделы

Аффилиация

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