add_div_of_nonneg_right

Mathlib.Data.EReal.Inv

URI: https://scilib.ai/kg/mathlib#EReal.add_div_of_nonneg_right

← MathLib Explorer

English

If c ≥ 0, then (a + b) / c = a / c + b / c for all a, b ∈ EReal.

Русский

Если c ≥ 0, то (a + b)/c = a/c + b/c для всех a, b ∈ EReal.

LaTeX

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

Lean4

theorem add_div_of_nonneg_right (h : 0 ≤ c) : (a + b) / c = a / c + b / c := by
  apply right_distrib_of_nonneg_of_ne_top (inv_nonneg_of_nonneg h) (inv_lt_top c).ne

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru