Theorems · Theorem · functional analysis

LineDeriv.lineDerivOpCLM_apply

∀ {R : Type u_4} {V : Type u_5} {E : Type u_6} {F : Type u_7} [inst : Ring R] [inst_1 : AddCommGroup E]
  [inst_2 : Module R E] [inst_3 : AddCommGroup F] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup V] [inst_8 : LineDeriv V E F] [inst_9 : LineDerivAdd V E F]
  [inst_10 : LineDerivSMul R V E F] [inst_11 : ContinuousLineDeriv V E F] (m : V) (x : E),
  (LineDeriv.lineDerivOpCLM R E m) x = LineDeriv.lineDerivOp m x

Defined in

Mathlib.Analysis.Distribution.DerivNotation

Cited by

0 results in Mathlib

Foundations

Depth 23 from the axioms · uses no axioms

Assumes

RingAddCommGroupModuleAddCommGroupModuleTopologicalSpaceTopologicalSpaceAddCommGroupLineDerivLineDerivAddLineDerivSMulContinuousLineDeriv