slope_neg_fun

Mathlib.LinearAlgebra.AffineSpace.Slope

URI: https://scilib.ai/kg/mathlib#slope_neg_fun

English

Slope of the negated function equals the negation of the slope: slope −f = − slope f.

Русский

Наклон для функции, заданной как −f, равен − наклону: slope(−f) = −slope(f).

LaTeX

$$$\operatorname{slope}(\Pi\!\!\!\!\!\!\!\!\!\! -f) = -\operatorname{slope}(f)$$$

Lean4

@[simp]
theorem slope_neg_fun (f : k → E) : slope (-f) = -slope f := by ext x y; exact slope_neg f x y

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

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

Разделы

Аффилиация

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