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).
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
forall e [>] 0, exists d [>] 0, forall (x : IR)
( [--]d [<] p[-]x [<] d) -> ( [--]e [<] [--]f(x) [<] e)
The limit of f in p is l if
forall e [>] 0, exists d [>] 0, forall (x : IR)
( [--]d [<] p[-]x [<] d) -> ( [--]e [<] [--]f(x) [<] e)
Definition funLim (p l : IR) : CProp := forall e, 0 [<] e ->
{d : IR | 0 [<] d | forall x, AbsSmall d (p[-]x) -> AbsSmall e (l[-]f x)}.
The definition of limit of f in p using Cauchy sequences.
Definition funLim_Cauchy (p l : IR) : CProp := forall s : CauchySeqR, Lim s [=] p ->
forall e, 0 [<] e -> {N : N | forall 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
forall e [>] 0, exists d [>] 0, forall (x : IR)
( [--]d [<] p[-]x [<] d) -> ( [--]d' [<] p'[-]y [<] d') -> ( [--]e [<] l[-]f(x,y) [<] e
forall e [>] 0, exists d [>] 0, forall (x : IR)
( [--]d [<] p[-]x [<] d) -> ( [--]d' [<] p'[-]y [<] d') -> ( [--]e [<] l[-]f(x,y) [<] e
Definition funLim2 (p p' l : IR) : CProp := forall e : IR, 0 [<] e -> {d : IR | 0 [<] d | forall 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 ε / δ 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 := forall x : IR, continAt x.
Definition continCauchy : CProp := forall x : IR, continAtCauchy x.
Definition contin2 : CProp := forall x y : IR, continAt2 x y.
Continuous on a closed, resp. open, resp. left open, resp. left closed
interval
Definition continOnc a b : CProp := forall x, Intclr a b x -> continAt x.
Definition continOno a b : CProp := forall x, Intolr a b x -> continAt x.
Definition continOnol a : CProp := forall x, Intol a x -> continAt x.
Definition continOncl a : CProp := forall x, Intcl a x -> continAt x.
End Continuity.