isBigO_map

Mathlib.Analysis.Asymptotics.Defs

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

English

Maps preserve Big-O: isBigO_map holds with simp lemmas

Русский

Отображения сохраняют Big-O: isBigO_map выполняется как упрощение

LaTeX

$$$@[simp] isBigO_map {k} {l} : f =O[map k l] g \iff (f \circ k) =O[l] (g \circ k) $$$

Lean4

@[simp]
theorem isBigO_map {k : β → α} {l : Filter β} : f =O[map k l] g ↔ (f ∘ k) =O[l] (g ∘ k) := by
  simp only [IsBigO_def, isBigOWith_map]

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

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

Разделы

Аффилиация

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