slope_vadd_const — Mathlib

English

Translating the codomain by a fixed point c does not change the slope: slope (f x +ᵥ c) = slope f.

Русский

Перенос значения функции на константу c не меняет наклон: slope (f x +ᵥ c) = slope f.

LaTeX

$$$\operatorname{slope}(\lambda x. f(x) +\!\!\!\!\!_v c) = \operatorname{slope}(f)$$$

Lean4

@[simp]
theorem slope_vadd_const (f : k → E) (c : PE) : (slope fun x => f x +ᵥ c) = slope f :=
  by
  ext a b
  simp only [slope, vadd_vsub_vadd_cancel_right, vsub_eq_sub]

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