sub_smul_dslope — Mathlib

English

Let f: 𝕜 → E be a function between a nontrivial normed field 𝕜 and a normed additive group E, and let a,b ∈ 𝕜. Then the increment of f along a,b is controlled by the slope: (b − a) times dslope f a b equals f(b) − f(a).

Русский

Пусть f: 𝕜 → E. Для любых a,b ∈ 𝕜 выполняется соотношение: (b − a) · dslope f a b = f(b) − f(a).

LaTeX

$$$(b - a) \cdot dslope\ f\ a\ b = f(b) - f(a)$$$

Lean4

@[simp]
theorem sub_smul_dslope (f : 𝕜 → E) (a b : 𝕜) : (b - a) • dslope f a b = f b - f a := by
  rcases eq_or_ne b a with (rfl | hne) <;> simp [dslope_of_ne, *]

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