mul_equiv_mul

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.mul_equiv_mul

← MathLib Explorer

English

If f1 ≈ f2 and g1 ≈ g2, then f1*g1 ≈ f2*g2.

Русский

Если f1 ≈ f2 и g1 ≈ g2, то f1·g1 ≈ f2·g2.

LaTeX

$$$ f_1 \approx f_2 \land g_1 \approx g_2 \Rightarrow f_1 g_1 \approx f_2 g_2 $$$

Lean4

theorem mul_equiv_mul {f1 f2 g1 g2 : CauSeq β abv} (hf : f1 ≈ f2) (hg : g1 ≈ g2) : f1 * g1 ≈ f2 * g2 := by
  simpa only [mul_sub, sub_mul, sub_add_sub_cancel] using add_limZero (mul_limZero_left g1 hf) (mul_limZero_right f2 hg)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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