|
%------------------------------------------------------------------------------
% Metric space
%
% Author: David Lester, Manchester University
%
% Version 1.0 5/12/04 Initial Version
% Version 1.1 15/06/09 All Proofs discharged (DRL)
%------------------------------------------------------------------------------
metric_space[T:TYPE, (IMPORTING metric_def[T]) d:metric]: THEORY
BEGIN
IMPORTING metric_def[T],
topology@topology_def[T],
metric_space_def[T,d]
S: VAR set[T]
x,y,z: VAR T
r: VAR posreal
metric_open_set:set[T] = emptyset[T]
metric_closed_set:set[T] = complement(metric_open_set)
metric_zero: LEMMA d(x,y) = 0 <=> x = y
metric_symmetric: LEMMA d(x,y) = d(y,x)
metric_triangle: LEMMA d(x,z) <= d(x,y) + d(y,z)
metric_is_0: LEMMA d(x,x) = 0
ball_centre: LEMMA member(x,ball(x,r))
metric_open_ball: LEMMA metric_open?(ball(x,r))
metric_open: TYPE+ = (metric_open?) CONTAINING metric_open_set
metric_closed: TYPE+ = (metric_closed?) CONTAINING metric_closed_set
ball_is_metric_open: JUDGEMENT ball(x,r) HAS_TYPE metric_open
metric_space_is_topology?: JUDGEMENT metric_induced_topology
HAS_TYPE (topology?)
metric_space_is_hausdorff?: JUDGEMENT metric_induced_topology
HAS_TYPE (hausdorff?)
metric_space_is_topology:
JUDGEMENT metric_induced_topology HAS_TYPE topology
metric_space_is_hausdorff:
JUDGEMENT metric_induced_topology HAS_TYPE hausdorff
IMPORTING topology@topology[T,(metric_induced_topology)]
metric_open_def: LEMMA metric_open?(S) <=> open?(S)
metric_closed_def: LEMMA metric_closed?(S) <=> closed?(S)
metric_open_is_open: JUDGEMENT metric_open SUBTYPE_OF open
open_is_metric_open: JUDGEMENT open SUBTYPE_OF metric_open
metric_closed_is_closed: JUDGEMENT metric_closed SUBTYPE_OF closed
closed_is_metric_closed: JUDGEMENT closed SUBTYPE_OF metric_closed
metric_adherent_iff_adherent: LEMMA
metric_adherent?(x,S) <=> adherent_point?(x,S)
metric_closure_is_Cl: LEMMA metric_closure(S) = Cl(S)
IMPORTING topology@hausdorff_convergence[T,(metric_induced_topology)],
sets_aux@countable_setofsets, % proof only
sets_aux@countable_image, % proof only
countable_cross % proof only
u,v: VAR sequence[T]
metric_convergence_def: LEMMA convergence?(u,x) <=> metric_converges_to(u,x)
weierstrass_bolzano?:bool
= FORALL u: EXISTS v: subseq?(v,u) AND metric_convergent?(v)
compact_is_weierstrass_bolzano: LEMMA % SKB 6.1.11
compact?(fullset[T]) => weierstrass_bolzano?
cauchy_subseq_is_totally_bounded: LEMMA % SKB 6.1.17
(FORALL u: EXISTS v: cauchy?(v) AND subseq?(v,u)) =>
totally_bounded?(fullset[T])
totally_bounded_is_separable: LEMMA % SKB 6.1.19
totally_bounded?(fullset[T]) => separable?(fullset[T])
separable_has_countable_basis: LEMMA % SKB 6.1.21
separable?(fullset[T]) => has_countable_basis?(metric_induced_topology)
IMPORTING topology@lindelof, % Proof Only
sets_aux@nat_indexed_sets[T], % Proof Only
sets_aux@countable_indexed_sets[T] % Proof Only
compact_iff_convergent_subseq: LEMMA % SKB 6.1.23
compact?(fullset[T]) <=> weierstrass_bolzano?
totally_bounded_iff_cauchy_subseq: LEMMA % SKB 6.1.24
totally_bounded?(fullset[T]) <=>
FORALL u: EXISTS v: cauchy?(v) AND subseq?(v,u)
compact_is_complete_totally_bounded: LEMMA % SKB 6.1.26
compact?(fullset[T]) <=>
metric_complete?(fullset[T]) AND totally_bounded?(fullset[T])
metric_complete: TYPE = (complete_metric_space?[T,d])
END metric_space
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
