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

Definition df-ditg 21722
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 21721 . 2
6 cle 9556 . . . 4
72, 3, 6wbr 4409 . . 3
8 cioo 11439 . . . . 5
92, 3, 8co 6222 . . . 4
101, 9, 4citg 21498 . . 3
113, 2, 8co 6222 . . . . 5
121, 11, 4citg 21498 . . . 4
1312cneg 9733 . . 3
147, 10, 13cif 3905 . 2
155, 14wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  ditgeq1  21723  ditgeq2  21724  ditgeq3  21725  ditgex  21727  ditg0  21728  cbvditg  21729  ditgpos  21731  ditgneg  21732  ditgeq3d  30511
  Copyright terms: Public domain W3C validator