The norm of a function is defined as being the supremum of its absolute value; that is equivalent to the following definition (which is often more convenient to use).
*)
(*#*
The norm of a function is defined as being the supremum of its absolute value; that is equivalent to the following definition (which is often more convenient to use).
We now prove some basic properties of the norm---namely that it is positive, and that it provides a least upper bound for the absolute value of its argument.
*)
(*#*
We now prove some basic properties of the norm---namely that it is positive, and that it provides a least upper bound for the absolute value of its argument.
+alias id "incF" = "cic:/CoRN/ftc/Continuity/Local_Results/incF.var".
-inline cic:/CoRN/ftc/Continuity/incG.var.
+alias id "incG" = "cic:/CoRN/ftc/Continuity/Local_Results/incG.var".
(*#*
The first result does not require the function to be continuous; however, its preconditions are easily verified by continuous functions, which justifies its inclusion in this section.
*)
(*#*
The first result does not require the function to be continuous; however, its preconditions are easily verified by continuous functions, which justifies its inclusion in this section.
Assume [F] and [G] are continuous in [I]. Then functions derived from these through algebraic operations are also continuous, provided (in the case of reciprocal and division) some extra conditions are met.
*)
(*#*
Assume [F] and [G] are continuous in [I]. Then functions derived from these through algebraic operations are also continuous, provided (in the case of reciprocal and division) some extra conditions are met.
*)
-inline cic:/CoRN/ftc/Continuity/contF.var.
+alias id "contF" = "cic:/CoRN/ftc/Continuity/Local_Results/contF.var".
-inline cic:/CoRN/ftc/Continuity/contG.var.
+alias id "contG" = "cic:/CoRN/ftc/Continuity/Local_Results/contG.var".