Definition df-ditg

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)

	Ref	Expression
Assertion	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

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2		cC	|- C
3		vx	|- x
4	3 0 1 2	cdit	|- S_ [ A -> B ] C _d x
5		cle	|- <_
6	0 1 5	wbr	|- A <_ B
7		cioo	|- (,)
8	0 1 7	co	|- ( A (,) B )
9	3 8 2	citg	|- S. ( A (,) B ) C _d x
10	1 0 7	co	|- ( B (,) A )
11	3 10 2	citg	|- S. ( B (,) A ) C _d x
12	11	cneg	|- -u S. ( B (,) A ) C _d x
13	6 9 12	cif	|- if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x )
14	4 13	wceq	|- S_ [ A -> B ] C _d x = if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x )