MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ditg Unicode version

Definition df-ditg 18996
Description: Define the directed integral, which is just a regular integral but with a sign change when the limits are interchanged. The  A and  B here are the lower and upper limits of the integral, usually written as a subscript and superscript next to the integral sign. We define the region of integration to be an open interval instead of closed so that we can use  +oo ,  -oo for limits and also integrate up to a singularity at an endpoint. (Contributed by Mario Carneiro, 13-Aug-2014.)
Assertion
Ref Expression
df-ditg  |-  S__ [ A  ->  B ] C  _d x  =  if ( A  <_  B ,  S. ( A (,) B
) C  _d x ,  -u S. ( B (,) A ) C  _d x )

Detailed syntax breakdown of Definition df-ditg
StepHypRef Expression
1 vx . . 3  set  x
2 cA . . 3  class  A
3 cB . . 3  class  B
4 cC . . 3  class  C
51, 2, 3, 4cdit 18990 . 2  class  S__ [ A  ->  B ] C  _d x
6 cle 8884 . . . 4  class  <_
72, 3, 6wbr 4039 . . 3  wff  A  <_  B
8 cioo 10672 . . . . 5  class  (,)
92, 3, 8co 5874 . . . 4  class  ( A (,) B )
101, 9, 4citg 18989 . . 3  class  S. ( A (,) B ) C  _d x
113, 2, 8co 5874 . . . . 5  class  ( B (,) A )
121, 11, 4citg 18989 . . . 4  class  S. ( B (,) A ) C  _d x
1312cneg 9054 . . 3  class  -u S. ( B (,) A ) C  _d x
147, 10, 13cif 3578 . 2  class  if ( A  <_  B ,  S. ( A (,) B
) C  _d x ,  -u S. ( B (,) A ) C  _d x )
155, 14wceq 1632 1  wff  S__ [ A  ->  B ] C  _d x  =  if ( A  <_  B ,  S. ( A (,) B
) C  _d x ,  -u S. ( B (,) A ) C  _d x )
Colors of variables: wff set class
This definition is referenced by:  ditgeq1  19214  ditgeq2  19215  ditgeq3  19216  ditgex  19218  ditg0  19219  cbvditg  19220  ditgpos  19222  ditgneg  19223
  Copyright terms: Public domain W3C validator