div_right_distrib_of_nonneg — Mathlib

English

Let a, b, c be elements of EReal with a ≥ 0 and b ≥ 0. Then (a + b) / c = a / c + b / c.

Русский

Пусть a, b, c принадлежат EReal и a ≥ 0, b ≥ 0. Тогда (a + b)/c = a/c + b/c.

LaTeX

$$$\\\\forall a,b,c \\\\in \\\\mathrm{EReal},\\ a \\\\ge 0, \\\\ b \\\\ge 0 \\\\Rightarrow \\\\frac{a+b}{c} = \\frac{a}{c} + \\frac{b}{c}$$$

Lean4

theorem div_right_distrib_of_nonneg (h : 0 ≤ a) (h' : 0 ≤ b) : (a + b) / c = a / c + b / c :=
  EReal.right_distrib_of_nonneg h h'

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