limit_mul_val — Mathlib

English

The limit inherits a group operation coordinatewise: for x,y in the limit, (x*y).val j = x.val j * y.val j for each j.

Русский

Предел наследует операцию умножения по координатам: для элементов x,y предела выполняется (x*y).val_j = x.val_j · y.val_j.

LaTeX

$$$\forall x,y:\mathrm{limit}(F),\; (x\cdot y).\mathrm{val}(j) = x(j) \cdot y(j)$$$

Lean4

@[simp]
theorem limit_mul_val (x y : limit F) (j : J) : (x * y).val j = x.val j * y.val j :=
  rfl

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