isLittleO_map

Mathlib.Analysis.Asymptotics.Defs

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

English

IsLittleO is preserved under map: f = o[l] g iff f ∘ k = o[l] g ∘ k

Русский

Малая-O сохраняется через отображение: f = o[l] g эквивалентно f ∘ k = o[l] g ∘ k

LaTeX

$$$ f = o[l] g \iff (f \circ k) = o[l] (g \circ k) $$$

Lean4

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

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

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

Разделы

Аффилиация

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