mul_sub

Mathlib.Data.ENNReal.Operations

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

English

If 0 < c and c < b and a ≠ ∞, then a*(b − c) = a*b − a*c.

Русский

Если 0 < c и c < b и a ≠ ∞, то a·(b − c) = a·b − a·c.

LaTeX

$$$ (0 < c) \land (c < b) \land (a \neq \infty) \Rightarrow a (b - c) = a b - a c $$$

Lean4

protected theorem mul_sub (h : 0 < c → c < b → a ≠ ∞) : a * (b - c) = a * b - a * c :=
  by
  simp only [mul_comm a]
  exact ENNReal.sub_mul h

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

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

Разделы

Аффилиация

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