|
%------------------------------------------------------------------------------
% Metric Spaces for Vector[n]
%
% Author: David Lester, Manchester University
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
% Version 1.0 17/08/07 Initial Version
%------------------------------------------------------------------------------
euclidean[n:posnat]: THEORY
BEGIN
IMPORTING vectors@vectors[n],
reals@sigma[below[n]],
reals@sqrt,
reals@bounded_reals,
metric_def[Vector],
metric_space_def
X: VAR set[Vector]
x,y,z: VAR Vector
i: VAR below[n]
r: VAR posreal
sigma_nnreal_eq_0: LEMMA FORALL (f:[below[n]->nnreal]):
sigma(0,n-1,f) = 0 <=> (FORALL i: f(i) = 0)
d1:metric = LAMBDA x,y: sigma(0,n-1,(LAMBDA i: abs(x(i)-y(i))))
d2:metric = LAMBDA x,y: sqrt(sigma(0,n-1,(LAMBDA i: sq(x(i)-y(i)))))
dinf:metric = LAMBDA x,y: max({z:nnreal | EXISTS i: abs(x(i)-y(i)) = z})
euclidean_d1: LEMMA metric_space?[Vector,d1](fullset[Vector])
euclidean_d2: LEMMA metric_space?[Vector,d2](fullset[Vector])
euclidean_dinf: LEMMA metric_space?[Vector,dinf](fullset[Vector])
% We now show that R^n has a countable basis.
Qn : TYPE+ = [Index->rat] CONTAINING zero
Qn_is_Vector: JUDGEMENT Qn SUBTYPE_OF Vector
q: VAR Qn
pq: VAR posrat
IMPORTING metric_space[Vector,d2],
countable_cross, % Proof Only
sets_aux@countable_types % Proof only
Qn_countable: LEMMA is_countable(fullset[Qn])
balls: TYPE+ = {X | EXISTS x,r: X = ball(x,r)} CONTAINING
ball[Vector,d2](zero,1)
rational_balls: TYPE+ = {X | EXISTS q,pq: X = ball[Vector,d2](q,pq)}
CONTAINING ball[Vector,d2](zero,1)
ball_basis: LEMMA base?(metric_induced_topology[Vector,d2])(fullset[balls])
% WAS: Qn_dense: LEMMA dense_in?(fullset[Qn],fullset[Vector])
Qn_dense: LEMMA dense_in?({x | EXISTS q: x=q},fullset[Vector])
Qn_basis: LEMMA
base?(metric_induced_topology[Vector,d2])(fullset[rational_balls])
countable_rational_balls: LEMMA is_countable(fullset[rational_balls])
euclidean_topology_is_second_countable:
JUDGEMENT metric_induced_topology[Vector,d2] HAS_TYPE second_countable
IMPORTING complete_product, % Proof only
real_topology, % Proof only
vectors@vectors, % Proof only
reals@sigma % Proof only
euclidean_topology_is_complete:
JUDGEMENT fullset[Vector[n]] HAS_TYPE metric_complete[Vector[n],d2]
END euclidean
¤ Dauer der Verarbeitung: 0.1 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.
|
