Registered elementary functions

The standard elementary functions use the same enclosure registration as user-defined operations. Their procedures and containment proofs reuse the existing endpoint-independent backend contracts.

theorem FloatLib.Numerics.Interval.exp_extension_sound : (Backend.elementaryExtension UnaryOp.exp).Sound Real.exp

The registered exp enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.log_extension_sound : (Backend.elementaryExtension UnaryOp.log).Sound Real.log

The registered log enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.sin_extension_sound : (Backend.elementaryExtension UnaryOp.sin).Sound Real.sin

The registered sin enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.cos_extension_sound : (Backend.elementaryExtension UnaryOp.cos).Sound Real.cos

The registered cos enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.tan_extension_sound : (Backend.elementaryExtension UnaryOp.tan).Sound Real.tan

The registered tan enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.arcsin_extension_sound : (Backend.elementaryExtension UnaryOp.asin).Sound Real.arcsin

The registered arcsin enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.arccos_extension_sound : (Backend.elementaryExtension UnaryOp.acos).Sound Real.arccos

The registered arccos enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.arctan_extension_sound : (Backend.elementaryExtension UnaryOp.atan).Sound Real.arctan

The registered arctan enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.sinh_extension_sound : (Backend.elementaryExtension UnaryOp.sinh).Sound Real.sinh

The registered sinh enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.cosh_extension_sound : (Backend.elementaryExtension UnaryOp.cosh).Sound Real.cosh

The registered cosh enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.tanh_extension_sound : (Backend.elementaryExtension UnaryOp.tanh).Sound Real.tanh

The registered tanh enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.sqrt_extension_sound : (Backend.elementaryExtension UnaryOp.sqrt).Sound Real.sqrt

The registered sqrt enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.arsinh_extension_sound : Backend.asinhExtension.Sound Real.arsinh

The registered arsinh enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.arcosh_extension_sound : Backend.acoshExtension.Sound Real.arcosh

The registered arcosh enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.artanh_extension_sound : Backend.atanhExtension.Sound Real.artanh

The registered artanh enclosure contains every accepted real input's image.

theorem FloatLib.Numerics.Interval.rpow_extension_sound : Backend.rpowExtension.Sound Real.rpow

The registered rpow enclosure contains every accepted pair of real inputs.

theorem FloatLib.Numerics.Interval.logb_extension_sound : Backend.logbExtension.Sound Real.logb

The registered logb enclosure contains every accepted pair of real inputs.