| products/sources/formale Sprachen/PVS/lnexp_fnd/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: normal_subgroups.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
%------------------------------------------------------------------------------
% 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.21 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.Bot Zugriff |
