isLittleO_bot

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.isLittleO_bot

English

If f = O_l g' and f = O_{l'} g', then f = O_{l ⊔ l'} g'.

Русский

Если f = O_l g' и f = O_{l'} g', тогда f = O_{l ⊔ l'} g'.

LaTeX

$$$\;\text{If } f =O_l g'\text{ and } f =O_{l'} g'\text{ then } f =O_{l \sqcup l'} g'.$$$

Lean4

@[simp]
theorem isLittleO_bot : f =o[⊥] g :=
  IsLittleO.of_isBigOWith fun c _ => isBigOWith_bot c f g

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

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

Разделы

Аффилиация

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