mul

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsEquivalent.mul

English

If t ~_l u and v ~_l w, then t · v ~_l u · w (pointwise product).

Русский

Если t ~_l u и v ~_l w, то t·v ~_l u·w.

LaTeX

$$$ (t \\sim_{l} u) \\land (v \\sim_{l} w) \\Rightarrow (t \\cdot v) \\sim_{l} (u \\cdot w) $$$

Lean4

protected theorem mul (htu : t ~[l] u) (hvw : v ~[l] w) : t * v ~[l] u * w :=
  htu.smul hvw

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

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

Разделы

Аффилиация

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