isTheta_refl

Mathlib.Analysis.Asymptotics.Theta

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

English

A simp lemma establishing a basic coordinatewise equivalence for BigOTVS on a pi-type.

Русский

Лемма simp, устанавливающая базовую координатную эквивалентность для BigOTVS на pi-типе.

LaTeX

$$$ f =O_{𝕜;l} g \iff ∀ i, f_i =O_{𝕜;l} g. $$$

Lean4

@[refl]
theorem isTheta_refl (f : α → E) (l : Filter α) : f =Θ[l] f :=
  ⟨isBigO_refl _ _, isBigO_refl _ _⟩

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

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

Разделы

Аффилиация

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