bot

Mathlib.Analysis.Asymptotics.TVS

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsLittleOTVS.bot

English

If f and g are little-OTVS relative to k, then the pair (f, g) is little-OTVS relative to k as a product.

Русский

Если f и g являются LittleOTVS относительно k, то пара (f,g) тожеLittleOTVS относительно k.

LaTeX

$$$f =o[𝕜; l] k \\land g =o[𝕜; l] k \\Rightarrow (f, g) =o[𝕜; l] k.$$$

Lean4

@[simp]
theorem bot : f =o[𝕜; ⊥] g :=
  ⟨fun u hU ↦ ⟨univ, by simp [EventuallyLE]⟩⟩

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

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

Разделы

Аффилиация

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