$\emptyset$#∅# for [a [>] b]).
*)
-inline procedural "cic:/CoRN/reals/RealFuncts/Intclr.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/Intclr.con" as definition.
-inline procedural "cic:/CoRN/reals/RealFuncts/Intolr.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/Intolr.con" as definition.
-inline procedural "cic:/CoRN/reals/RealFuncts/Intol.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/Intol.con" as definition.
-inline procedural "cic:/CoRN/reals/RealFuncts/Intcl.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/Intcl.con" as definition.
-inline procedural "cic:/CoRN/reals/RealFuncts/Intcr.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/Intcr.con" as definition.
(*#* The limit of [f(x)] as [x] goes to [p = l], for both unary and binary
functions:
]]
*)
-inline procedural "cic:/CoRN/reals/RealFuncts/funLim.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/funLim.con" as definition.
(*#* The definition of limit of [f] in [p] using Cauchy sequences. *)
-inline procedural "cic:/CoRN/reals/RealFuncts/funLim_Cauchy.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/funLim_Cauchy.con" as definition.
(*#* The first definition implies the second one. *)
]]
*)
-inline procedural "cic:/CoRN/reals/RealFuncts/funLim2.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/funLim2.con" as definition.
(*#* The function [f] is continuous at [p] if the limit of [f(x)] as
[x] goes to [p] is [f(p)]. This is the [eps [/] delta] definition.
We also give the definition with limits of Cauchy sequences.
*)
-inline procedural "cic:/CoRN/reals/RealFuncts/continAt.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continAt.con" as definition.
-inline procedural "cic:/CoRN/reals/RealFuncts/continAtCauchy.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continAtCauchy.con" as definition.
-inline procedural "cic:/CoRN/reals/RealFuncts/continAt2.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continAt2.con" as definition.
(*
Ax_iom continAt_prop1 :(p:IR)(continAt p)->(continAtCauchy p).
*)
-inline procedural "cic:/CoRN/reals/RealFuncts/contin.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/contin.con" as definition.
-inline procedural "cic:/CoRN/reals/RealFuncts/continCauchy.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continCauchy.con" as definition.
-inline procedural "cic:/CoRN/reals/RealFuncts/contin2.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/contin2.con" as definition.
(*#*
Continuous on a closed, resp.%\% open, resp.%\% left open, resp.%\% left closed
interval *)
-inline procedural "cic:/CoRN/reals/RealFuncts/continOnc.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continOnc.con" as definition.
-inline procedural "cic:/CoRN/reals/RealFuncts/continOno.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continOno.con" as definition.
-inline procedural "cic:/CoRN/reals/RealFuncts/continOnol.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continOnol.con" as definition.
-inline procedural "cic:/CoRN/reals/RealFuncts/continOncl.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continOncl.con" as definition.
(*
Section Sequence_and_function_limits.