lim_mul

Mathlib.Algebra.Order.CauSeq.Completion

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

English

Limit of a product with a fixed element: lim f · x = lim (f · const abv x).

Русский

Предел произведения с фиксированным элементом: lim f · x = lim (f · const abv x).

LaTeX

$$$\\lim f \\cdot x = \\lim (f \\cdot \\mathrm{const}(abv)\\, x)$$$

Lean4

theorem lim_mul (f : CauSeq β abv) (x : β) : lim f * x = lim (f * const abv x) := by rw [← lim_mul_lim, lim_const]

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

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

Разделы

Аффилиация

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