src/probability/real_topologyScript.sml

4953 (* Common nets and the "within" modifier for nets.                           *)
4956 val _ = set_fixity "within" (Infix(NONASSOC, 450));
4974 val within = new_definition ("within",
4975   ``(net within s) = mk_net(\x y. netord net x y /\ x IN s)``);
4978   ``(a in_direction v) = ((at a) within {b | ?c. &0 <= c /\ (b - a = c * v)})``);
5019  ``!n s x y. netord(n within s) x y <=> netord n x y /\ x IN s``,
5020   GEN_TAC THEN GEN_TAC THEN SIMP_TAC std_ss [within, GSYM FUN_EQ_THM] THEN
5031  ``!x:real. (at x within UNIV) = at x``,
5032   REWRITE_TAC[within, at, IN_UNIV] THEN REWRITE_TAC[ETA_AX, net_tybij]);
5035  ``!net s t. ((net within s) within t) = (net within (s INTER t))``,
5036   ONCE_REWRITE_TAC[within] THEN
5049  ``!a:real. trivial_limit (at a within s) <=> ~(a limit_point_of s)``,
5105  ``!a s. closed s /\ ~(a IN s) ==> trivial_limit (at a within s)``,
5109  ``!net s. trivial_limit net ==> trivial_limit(net within s)``,
5127      eventually p (at a within s) <=>
5142      eventually p (at a within s) <=>
5284         (f --> l)(at a within s) <=>
5292       (f --> l) (at a within s) <=>
5370  ``!f l x. (f --> l) (at x within {})``,
5375     (f --> l) (at a within s) /\ t SUBSET s ==> (f --> l) (at a within t)``,
5380         (f --> l) (at x within s) /\ (f --> l) (at x within t)
5381         ==> (f --> l) (at x within (s UNION t))``,
5392         (f --> l) (at x within s) /\ (f --> l) (at x within t) /\
5404     (g --> z) (at y within s)
5409    (!e. &0 < e ==> eventually (\x. dist (g x,z) < e) (at y within s))
5441  ``!f l a s. (f --> l)(at a) ==> (f --> l)(at a within s)``,
5446      a IN s /\ open s ==> ((f --> l)(at a within s) <=> (f --> l)(at a))``,
6243  ``!a s. ((\x. x) --> a) (at a within s)``,
6272  ``!a:real s. ~(trivial_limit (at a within s))
6273     ==> (netlimit (at a within s) = a)``,
6310   (f --> l) (at x within s) ==> (g --> l) (at x within s)``,
6336   ==> ((f --> l) (at a within s) <=> (f --> l) (at a within t))``,
6347   eventually (\x. x IN t ==> x IN s) (at a) /\ (f --> l) (at a within s)
6348   ==> (f --> l) (at a within t)``,
6364   (f --> l) (at a within s) ==> (g --> l) (at a within s)``,
6379 (* Alternatively, within an open set. *)
6397   (f --> l) (at a within t) ==> (g --> l) (at a within t)``,
6451   ==> (((\x. f x) --> l) (at a within s) <=> ((g --> l) (at a within s)))``,
6745   ==> (eventually p (at x within s) <=> eventually p (at x))``,
6755    ==> ((f --> l) (at x within s) <=> (f --> l) (at x))``,
6759  ``!s x:real. x IN interior s ==> (netlimit(at x within s) = x)``,
8604  ``!f x:real. f continuous (at x within s) <=> (f --> f(x)) (at x within s)``,
8606   ASM_CASES_TAC ``trivial_limit(at (x:real) within s)`` THENL
8616   f continuous (at x) ==> f continuous (at x within s)``,
8620  ``!a s. closed s /\ ~(a IN s) ==> f continuous (at a within s)``,
8626     f continuous (at x within s) ==> g continuous (at x within s)``,
8647     f continuous (at a within t) ==> g continuous (at a within t)``,
8652    f continuous (at a within s) ==> f continuous (at a within t)``,
8660  ``f continuous (at x within s) <=> !e. &0 < e
8678  ``!f s x. f continuous (at x within s) <=>
8697         g continuous (at a within s) /\
8699         ==> f continuous (at a within s)``,
8735  ``!f s. f continuous_on s <=> !x. x IN s ==> f continuous (at x within s)``,
8740   f continuous_on s <=> !x. x IN s ==> (f --> f(x)) (at x within s)``,
8749  ``!f s t x. f continuous (at x within s) /\ t SUBSET s
8750   ==> f continuous (at x within t)``,
8821     f continuous (at a within s) <=>
9251  ``!a s. (\x. x) continuous (at a within s)``,
9271  ``!f g x s. f continuous (at x within s) /\
9272       g continuous (at (f x) within IMAGE f s)
9273     ==> (g o f) continuous (at x within s)``,
9298     f continuous (at x within u) <=>
9533  ``!f:real->real s x. linear f ==> f continuous (at x within s)``,
11595         f continuous (at x within s) /\ x IN s /\  ~(f x = a)
11598   UNDISCH_TAC ``f continuous (at x within s)`` THEN DISCH_TAC THEN
13168         f continuous (at a within s) /\ ~(f a = &0)
13169         ==> (inv o f) continuous (at a within s)``,
13171   ASM_CASES_TAC ``trivial_limit (at (a:real) within s)`` THENL
15344  ``(f --> l) (at x within (s UNION t)) <=>
15345    (f --> l) (at x within s) /\ (f --> l) (at x within t)``,