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

Definition df-ditg 19517
 Description: Define the directed integral, which is just a regular integral but with a sign change when the limits are interchanged. The and 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 for limits and also integrate up to a singularity at an endpoint. (Contributed by Mario Carneiro, 13-Aug-2014.)
Assertion
Ref Expression
df-ditg _

Detailed syntax breakdown of Definition df-ditg
StepHypRef Expression
1 vx . . 3
2 cA . . 3
3 cB . . 3
4 cC . . 3
51, 2, 3, 4cdit 19511 . 2 _
6 cle 9121 . . . 4
72, 3, 6wbr 4212 . . 3
8 cioo 10916 . . . . 5
92, 3, 8co 6081 . . . 4
101, 9, 4citg 19510 . . 3
113, 2, 8co 6081 . . . . 5
121, 11, 4citg 19510 . . . 4
1312cneg 9292 . . 3
147, 10, 13cif 3739 . 2
155, 14wceq 1652 1 _
 Colors of variables: wff set class This definition is referenced by:  ditgeq1  19735  ditgeq2  19736  ditgeq3  19737  ditgex  19739  ditg0  19740  cbvditg  19741  ditgpos  19743  ditgneg  19744
 Copyright terms: Public domain W3C validator