Theorems · Definition · functional analysis

ContinuousLineDeriv.casesOn

{V : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : TopologicalSpace E] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : LineDeriv V E F] →
            {motive : ContinuousLineDeriv V E F → Sort u_1} →
              (t : ContinuousLineDeriv V E F) →
                ((continuous_lineDerivOp : ∀ (v : V), Continuous (LineDeriv.lineDerivOp v)) → motive ⋯) → motive t

Defined in

Mathlib.Analysis.Distribution.DerivNotation

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceLineDeriv