left_distrib_of_nonneg — Mathlib

English

Let a, b, c be elements of the extended real numbers with a ≥ 0 and b ≥ 0. Then c · (a + b) = c · a + c · b.

Русский

Пусть a, b, c ∈ EReal, причем a ≥ 0 и b ≥ 0. Тогда c · (a + b) = c · a + c · b.

LaTeX

$$$∀ a,b,c \in \mathrm{EReal},\; 0 \le a \land 0 \le b \Rightarrow c\cdot(a+b) = c\cdot a + c\cdot b$$$

Lean4

theorem left_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) : c * (a + b) = c * a + c * b :=
  by
  nth_rewrite 1 [EReal.mul_comm]; nth_rewrite 2 [EReal.mul_comm]; nth_rewrite 3 [EReal.mul_comm]
  exact right_distrib_of_nonneg ha hb

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