|
%------------------------------------------------------------------------------
% Metric Spaces
%
% Author: David Lester, Manchester University, NIA, Universite Perpignan
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
% Version 1.0 17/08/07 Initial Version
% Version 1.1 23/03/11 New intervals added for probability
%------------------------------------------------------------------------------
real_topology: THEORY
BEGIN
IMPORTING metric_space_def[real,(LAMBDA (x,y:real): abs(x-y))],
metric_space[real,(LAMBDA (x,y:real): abs(x-y))],
reals@bounded_reals,
countable_cross[rat,posrat], % Proof Only
sets_aux@countable_types % Proof only
a,x,y: VAR real
r: VAR posreal
q: VAR rat
pq: VAR posrat
X,A: VAR set[real]
interval?(A):bool = FORALL (x,y:(A),z:real): x <= z AND z <= y => A(z)
bounded?(A):bool
= (empty?(A) OR
(nonempty?(A) AND above_bounded[real](A) AND below_bounded[real](A)))
unbounded?(A):bool = NOT bounded?(A)
bounded_interval?(A):bool = interval?(A) AND bounded?(A)
unbounded_interval?(A):bool = interval?(A) AND unbounded?(A)
bounded_open_interval?(A):bool = bounded_interval?(A) and metric_open?(A)
interval: TYPE+ = (interval?) CONTAINING emptyset[real]
bounded_interval: TYPE+ = (bounded_interval?) CONTAINING emptyset[real]
unbounded_interval: TYPE+ = (unbounded_interval?) CONTAINING fullset[real]
bounded_open_interval:
TYPE+ = (bounded_open_interval?)CONTAINING emptyset[real]
open_interval: TYPE+ = {X | EXISTS x,r: X = ball(x,r)}
open_interval_is_bounded_open_interval:
JUDGEMENT open_interval SUBTYPE_OF bounded_open_interval
open_basis: LEMMA base?(metric_induced_topology)(fullset[open_interval])
rational_open_interval: TYPE+ = {X | EXISTS q,pq: X = ball(q,pq)}
rational_basis: LEMMA
base?(metric_induced_topology)(fullset[rational_open_interval])
countable_rational_open_interval: LEMMA
is_countable(fullset[rational_open_interval])
metric_induced_topology_is_second_countable:
JUDGEMENT metric_induced_topology HAS_TYPE second_countable
real_is_complete: JUDGEMENT fullset[real] HAS_TYPE metric_complete
closed_ball(x:real,r:nnreal):closed = {y | abs(x-y) <= r}
closed_interval: TYPE+ = {X | EXISTS (x:real,r:nnreal): X = closed_ball(x,r)}
open(a:real,b:{x | a < x}): open_interval = ball((a+b)/2,(b-a)/2)
closed(a:real,b:{x | a <= x}):closed_interval = closed_ball((a+b)/2,(b-a)/2)
open_inf(a):open = {x | a < x}
inf_open(a):open = {x | x < a}
reals:open = fullset[real]
posreals:open = open_inf(0)
negreals:open = inf_open(0)
closed_inf(a):closed = {x | a <= x}
inf_closed(a):closed = {x | x <= a}
nnreals:closed = closed_inf(0)
npreals:closed = inf_closed(0)
left_semiclosed_interval: TYPE+ = {X | EXISTS a: X = closed_inf(a)}
CONTAINING closed_inf(0)
right_semiclosed_interval: TYPE+ = {X | EXISTS a: X = inf_closed(a)}
CONTAINING inf_closed(0)
left_semiclosed_interval_is_interval:
JUDGEMENT left_semiclosed_interval SUBTYPE_OF interval
right_semiclosed_interval_is_interval:
JUDGEMENT right_semiclosed_interval SUBTYPE_OF interval
left_semiclosed_interval_is_closed:
JUDGEMENT left_semiclosed_interval SUBTYPE_OF closed
right_semiclosed_interval_is_closed:
JUDGEMENT right_semiclosed_interval SUBTYPE_OF closed
END real_topology
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
