sub_div

Mathlib.Data.ENNReal.Inv

URI: https://scilib.ai/kg/mathlib#ENNReal.sub_div

← MathLib Explorer

English

In ENNReal, if 0 < b < a and c ≠ 0, then (a - b)/c = a/c - b/c.

Русский

В ENNReal, если 0 < b < a и c ≠ 0, то (a - b)/c = a/c - b/c.

LaTeX

$$$0 < b \implies b < a \implies c \neq 0 \Rightarrow \dfrac{a-b}{c} = \dfrac{a}{c} - \dfrac{b}{c}$$$

Lean4

protected theorem sub_div (h : 0 < b → b < a → c ≠ 0) : (a - b) / c = a / c - b / c :=
  by
  simp_rw [div_eq_mul_inv]
  exact ENNReal.sub_mul (by simpa using h)

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

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

Разделы

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

Аффилиация

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