right_distrib_of_nonneg_of_ne_top

English

Let x, y, z be elements of the extended real numbers with x nonnegative and not equal to the top element. Then (y + z) · x = y · x + z · x.

Русский

Пусть x, y, z принадлежат расширенным вещественным числам, причём x неотрицательно и x ≠ верхний элемент. Тогда (y + z) · x = y · x + z · x.

LaTeX

$$$\\forall x,y,z \\in \\overline{\\mathbb{R}},\\ (0 \\le x \\land x \\neq \\infty) \\Rightarrow (y+z)\\cdot x = y\\cdot x + z\\cdot x$$$

Lean4

theorem right_distrib_of_nonneg_of_ne_top {x : EReal} (hx_nonneg : 0 ≤ x) (hx_ne_top : x ≠ ⊤) (y z : EReal) :
    (y + z) * x = y * x + z * x := by
  simpa only [EReal.mul_comm] using left_distrib_of_nonneg_of_ne_top hx_nonneg hx_ne_top y z

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