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

Definition df-ditg 22117
 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 22116 . 2 _
6 cle 9627 . . . 4
72, 3, 6wbr 4433 . . 3
8 cioo 11533 . . . . 5
92, 3, 8co 6277 . . . 4
101, 9, 4citg 21893 . . 3
113, 2, 8co 6277 . . . . 5
121, 11, 4citg 21893 . . . 4
1312cneg 9806 . . 3
147, 10, 13cif 3922 . 2
155, 14wceq 1381 1 _
 Colors of variables: wff setvar class This definition is referenced by:  ditgeq1  22118  ditgeq2  22119  ditgeq3  22120  ditgex  22122  ditg0  22123  cbvditg  22124  ditgpos  22126  ditgneg  22127  ditgeq3d  31649
 Copyright terms: Public domain W3C validator