mul_right — Mathlib

English

If c is a function from σ to S and x has evaluation, then x multiplied by c has evaluation (under an appropriate linear topology).

Русский

Если c — функция σ→S и у x есть оценка, то x умноженное на c имеет оценку при подходящей линейной топологии.

LaTeX

$$$\\text{HasEval } x \\Rightarrow \\text{HasEval } (x \\cdot c)$$$

Lean4

theorem mul_right [IsLinearTopology S S] (c : σ → S) {x : σ → S} (hx : HasEval x) : HasEval (x * c) :=
  mul_comm x c ▸ HasEval.mul_left c hx

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