CoRN.reals.RealFuncts
Let f be a unary setoid operation on IR and
let f2 be a binary setoid operation on IR.
We use the following notations for intervals. Intclr a b for the
closed interval [a,b], Intolr a b for the
open interval (a,b), Intcl a for the
left-closed interval [a,∞), Intol a for the
left-open interval (a,∞), Intcr b for the
right-closed interval (-∞,b].
Intervals like [a,b] are defined for arbitrary reals a,b (being
∅ for a [>] b).
Definition Intclr (a b x : IR) : Prop := a [<=] x ∧ x [<=] b.
Definition Intolr (a b x : IR) : CProp := a [<] x and x [<] b.
Definition Intol (a x : IR) : CProp := a [<] x.
Definition Intcl (a x : IR) : Prop := a [<=] x.
Definition Intcr (b x : IR) : Prop := x [<=] b.
The limit of f(x) as x goes to p = l, for both unary and binary
functions:
The limit of f in p is l if
∀ e [>] [0], ∃ d [>] [0], ∀ (x : IR)
( [--]d [<] p[-]x [<] d) → ( [--]e [<] [--]f(x) [<] e)
∀ e [>] [0], ∃ d [>] [0], ∀ (x : IR)
( [--]d [<] p[-]x [<] d) → ( [--]e [<] [--]f(x) [<] e)
Definition funLim (p l : IR) : CProp := ∀ e, [0] [<] e →
{d : IR | [0] [<] d | ∀ x, AbsSmall d (p[-]x) → AbsSmall e (l[-]f x)}.
Definition funLim_Cauchy (p l : IR) : CProp := ∀ s : CauchySeqR, Lim s [=] p →
∀ e, [0] [<] e → {N : nat | ∀ m, N ≤ m → AbsSmall e (f (s m) [-]l)}.
The first definition implies the second one.
The limit of f in (p,p') is l if
∀ e [>] [0], ∃ d [>] [0], ∀ (x : IR)
( [--]d [<] p[-]x [<] d) → ( [--]d' [<] p'[-]y [<] d') → ( [--]e [<] l[-]f(x,y) [<] e
∀ e [>] [0], ∃ d [>] [0], ∀ (x : IR)
( [--]d [<] p[-]x [<] d) → ( [--]d' [<] p'[-]y [<] d') → ( [--]e [<] l[-]f(x,y) [<] e
Definition funLim2 (p p' l : IR) : CProp := ∀ e : IR, [0] [<] e → {d : IR | [0] [<] d | ∀ x y,
AbsSmall d (p[-]x) → AbsSmall d (p'[-]y) → AbsSmall e (l[-]f2 x y)}.
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.
Definition continAt (p : IR) : CProp := funLim p (f p).
Definition continAtCauchy (p : IR) : CProp := funLim_Cauchy p (f p).
Definition continAt2 (p q : IR) : CProp := funLim2 p q (f2 p q).
Definition contin : CProp := ∀ x : IR, continAt x.
Definition continCauchy : CProp := ∀ x : IR, continAtCauchy x.
Definition contin2 : CProp := ∀ x y : IR, continAt2 x y.
Continuous on a closed, resp. open, resp. left open, resp. left closed
interval