right_distrib_of_nonneg — Mathlib

English

If 0 ≤ a and 0 ≤ b, then (a + b) * c = a * c + b * c.

Русский

Если 0 ≤ a и 0 ≤ b, то (a + b) * c = a * c + b * c.

LaTeX

$$0 \le a \land 0 \le b \Rightarrow (a + b) * c = a * c + b * c$$

Lean4

theorem right_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a + b) * c = a * c + b * c :=
  by
  lift a to ℝ≥0∞ using ha
  lift b to ℝ≥0∞ using hb
  cases c using recENNReal with
  | coe c => exact_mod_cast add_mul a b c
  | neg_coe c hc =>
    simp only [mul_neg, ← coe_ennreal_add, ← coe_ennreal_mul, add_mul]
    rw [coe_ennreal_add, EReal.neg_add (.inl (coe_ennreal_ne_bot _)) (.inr (coe_ennreal_ne_bot _)), sub_eq_add_neg]

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