Theorems · Definition · geometry

slope

{k : Type u_1} →
  {E : Type u_2} →
    {PE : Type u_3} →
      [inst : Field k] → [inst_1 : AddCommGroup E] → [Module k E] → [AddTorsor E PE] → (k → PE) → k → k → E

slope f a b = (b - a)⁻¹ • (f b -ᵥ f a) is the slope of a function f on the interval [a, b]. Note that slope f a a = 0, not the derivative of f at a.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Slope

Cited by

147 results in Mathlib

Foundations

Depth 45 from the axioms, rests on 540 definitions · uses propext, Classical.choice, Quot.sound

Assumes

FieldAddCommGroupModuleAddTorsor