IndisputableMonolith.Cost.Ndim.ScalarCertificates

declarations in this module (19)

• def P00 L55
• def dP00 L59
• def nablaP000 L63
• def R0101Closed L67
• theorem hasDerivAt_P00 L75
• theorem dP00_ne_zero L84
• theorem nablaP000_ne_zero L95
• theorem R0101Closed_neg L111
• def P00Gen L146
• def dP00Gen L149
• def kappaGen L155
• def nablaP000Gen L159
• def R0101Gen L164
• theorem kappaGen_pos L171
• theorem sinh_cross_pos L185
• theorem hasDerivAt_P00Gen L212
• theorem dP00Gen_ne_zero L228
• theorem nablaP000Gen_ne_zero L245
• theorem R0101Gen_neg L269