mul

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.Infinitesimal.mul

English

Product of two infinitesimals is infinitesimal.

Русский

Произведение двух бесконечно малых чисел бесконечно мало.

LaTeX

$$$\\forall {x y : \\mathbb{R}^*}, x \\text{ infinitesimal} \\land y \\text{ infinitesimal} \\rightarrow (x y) \\text{ infinitesimal}$$$

Lean4

nonrec theorem mul {x y : ℝ*} (hx : Infinitesimal x) (hy : Infinitesimal y) : Infinitesimal (x * y) := by
  simpa only [mul_zero] using hx.mul hy

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

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

Разделы

Аффилиация

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