members of the interval [[Min(a,b),Max(a,b)]].
*)
members of the interval [[Min(a,b),Max(a,b)]].
*)
(*#*
As we will be interested in taking functions with domain in a compact
interval, we want this predicate to be well defined.
*)
(*#*
As we will be interested in taking functions with domain in a compact
interval, we want this predicate to be well defined.
*)
(*#*
Suprema and infima will be needed throughout; we define them here both
for arbitrary subsets of [IR] and for images of functions.
*)
(*#*
Suprema and infima will be needed throughout; we define them here both
for arbitrary subsets of [IR] and for images of functions.
*)
(*#* The following lemma is a bit more specific: it shows that we can
also estimate the distance from the center of a compact interval to
any of its points. *)
(*#* The following lemma is a bit more specific: it shows that we can
also estimate the distance from the center of a compact interval to
any of its points. *)
(*#* Finally, two more useful lemmas to prove inclusion of compact
intervals. They will be necessary for the definition and proof of the
elementary properties of the integral. *)
(*#* Finally, two more useful lemmas to prove inclusion of compact
intervals. They will be necessary for the definition and proof of the
elementary properties of the integral. *)