isTheta_zero_right

Mathlib.Analysis.Asymptotics.Theta

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

English

Similarly, f'' =Θ_l 0 is equivalent to f'' =ᶠ_l 0 on the right.

Русский

Аналогично, f'' =Θ_l 0 эквивалентно f'' =ᶠ_l 0 справа.

LaTeX

$$$ (f'' =Θ[l] 0) \iff (f'' =\!\!\!_l 0). $$$

Lean4

@[simp]
theorem isTheta_zero_right : (f'' =Θ[l] fun _ ↦ (0 : F')) ↔ f'' =ᶠ[l] 0 :=
  isTheta_comm.trans isTheta_zero_left

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

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

Разделы

Аффилиация

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