Description: Two functions defined on a ball whose derivatives are the same and which are equal at any given point C in the ball must be equal everywhere. (Contributed by Mario Carneiro, 31-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dv11cn.x | |
|
dv11cn.a | |
||
dv11cn.r | |
||
dv11cn.f | |
||
dv11cn.g | |
||
dv11cn.d | |
||
dv11cn.e | |
||
dv11cn.c | |
||
dv11cn.p | |
||
Assertion | dv11cn | |