isBoundedUnder_le_iff

Mathlib.Analysis.Asymptotics.Theta

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsTheta.isBoundedUnder_le_iff

← MathLib Explorer

English

If f =Θ[l] g and l' ≤ l then f =Θ[l'] g.

Русский

Если f =Θ[l] g и l' ≤ l, то f =Θ[l'] g.

LaTeX

$$$ f =Θ[l] g \Rightarrow (l' \leq l) \Rightarrow f =Θ[l'] g. $$$

Lean4

theorem isBoundedUnder_le_iff (h : f' =Θ[l] g') :
    IsBoundedUnder (· ≤ ·) l (norm ∘ f') ↔ IsBoundedUnder (· ≤ ·) l (norm ∘ g') := by
  simp only [← isBigO_const_of_ne (one_ne_zero' ℝ), h.isBigO_congr_left]

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

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

Разделы

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

Аффилиация

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