isTheta_norm_left

Mathlib.Analysis.Asymptotics.Theta

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

English

If f ≡_l,g eventually, then f =Θ_l g.

Русский

Если f эквивалентны g поздно по отношению к l, то f =Θ_l g.

LaTeX

$$$f =\\Theta_l g$$$

Lean4

@[simp]
theorem isTheta_norm_left : (fun x ↦ ‖f' x‖) =Θ[l] g ↔ f' =Θ[l] g := by simp [IsTheta]

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

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

Разделы

Аффилиация

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