isLittleO_norm_right

Mathlib.Analysis.Asymptotics.Defs

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

← MathLib Explorer

English

The same equivalence as IsLittleO_norm_right but stated with simp-friendly form.

Русский

Та же эквивалентность, выраженная иначе через норму.

LaTeX

$$$\text{(IsLittleO l f (norm g'))} \iff \text{IsLittleO l f g'}$$$

Lean4

@[simp]
theorem isLittleO_norm_right : (f =o[l] fun x => ‖g' x‖) ↔ f =o[l] g' :=
  by
  simp only [IsLittleO_def]
  exact forall₂_congr fun _ _ => isBigOWith_norm_right

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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