isEquivalent_sin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

URI: https://scilib.ai/kg/mathlib#Complex.isEquivalent_sin

English

The function sin is asymptotically equivalent to the identity near 0: sin(x) ~ x as x → 0.

Русский

Функция sin близка к тождественной около 0: sin(x) ~ x при x → 0.

LaTeX

$$$$\text{IsEquivalent}(\mathcal{N}_0, \sin, \mathrm{id})$$$$

Lean4

theorem isEquivalent_sin : sin ~[𝓝 0] id := by simpa using (hasDerivAt_sin 0).isLittleO

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

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

Разделы

Аффилиация

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