Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/Pure/General/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 2 kB

Quellcode-Bibliothek metric_spaces.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Metric spaces definition file
%
%     Authors: David Lester, Manchester University & NIA
%              Anthony Narkawicz,  NASA Langley
%              Ricky Butler,       NASA Langley
%
%     Version 1.0            5/12/04  Initial Version
%     Version 1.1            8/18/09
%------------------------------------------------------------------------------

metric_spaces[T:TYPE+,d:[T,T->nnreal]]: THEORY
BEGIN

  ASSUMING IMPORTING metric_spaces_def[T,d]

%     metric_zero     : ASSUMPTION FORALL (x,y: T):   d(x,y)  = 0 IFF x = y
%     metric_symmetric: ASSUMPTION FORALL (x,y: T):   d(x,y)  = d(y,x)
%     metric_triangle : ASSUMPTION FORALL (x,y,z: T): d(x,z) <= d(x,y) + d(y,z)

      fullset_metric_space: ASSUMPTION metric_space?[T,d](fullset[T])

  ENDASSUMING

  IMPORTING prelude_sets_aux

  AUTO_REWRITE+  member
  AUTO_REWRITE+  complement_complement
  AUTO_REWRITE+  Complement_Complement

  metric_space: TYPE+ = set[T]

  r:     VAR posreal
  x,y,z: VAR T
  S,U:     VAR set[T]

  ball(x,r): set[T]          = {y | d(x,y) < r}

  interior_point?(x,S): bool = EXISTS r: subset?(ball(x,r),S)

  interior(S): set[T]        = {x:T | interior_point?(x,S) and S(x)}

  open?(S): bool             = interior(S) = S

  open_in?(S,U): bool      = (FORALL (s: (S)): EXISTS r: subset?(intersection(ball(s,r),U),S))
                               AND subset?(S,U)

  closed_in?(S,U): bool      = open_in?(intersection(complement(S),U),U) AND subset?(S,U)

  closed?(S): bool           = open?(complement(S))

  adherent_point?(x,S): bool = FORALL r: nonempty?(intersection(S,ball(x,r)))

  limit_point?(S)(x): bool    = adherent_point?(x,S) AND NOT member(x,S)

  metric_closure(S): set[T]  = {x:T | adherent_point?(x,S)}

  open_set:     TYPE  = (open?)
  closed_set:   TYPE  = (closed?)

  open_set_is_set:   JUDGEMENT open_set   SUBTYPE_OF set[T]
  closed_set_is_set: JUDGEMENT closed_set SUBTYPE_OF set[T]

  X:   VAR metric_space
  A,B: VAR set[T]

  % Mundane properties of open and closed sets

  open_emptyset:     LEMMA open?(emptyset)
  closed_emptyset:   LEMMA closed?(emptyset)
  complement_open:   LEMMA open?(A)   IFF closed?(complement(A))
  complement_closed: LEMMA closed?(A) IFF open?(complement(A))
  open_fullset:      LEMMA open?(fullset)
  closed_fullset:    LEMMA closed?(fullset)
  open_in_fullset:   LEMMA open?(A) IFF open_in?(A,fullset[T])
  closed_in_fullset: LEMMA closed?(A) IFF closed_in?(A,fullset[T])

  ball_open:         LEMMA open?(ball(x, r))

  Complement_open:   LEMMA FORALL (XS:set[open_set]):
                                                every(closed?)(Complement(XS))
  Complement_closed: LEMMA FORALL (XS:set[closed_set]):
                                                every(open?)(Complement(XS))

  subset_is_metric_space: LEMMA subset?(S,X) IMPLIES metric_space?(S)

  % Apostol 3.35a (1) (equivalent to Apostol 3.7 (generalized))
  % The union of any _collection_ of open sets is open

  open_Union_open: THEOREM FORALL (XS:set[open_set]): open?(Union(XS))

  % Apostol 3.35a (2) (equivalent to Apostol 3.8 (generalized))
  % The intersection of any _finite_set_ of open sets is open

  open_Intersection_open: THEOREM
               FORALL (FS:finite_set[open_set]): open?(Intersection(FS))

  % Apostol 3.35b (1) (equivalent to Apostol 3.7 (generalized))
  % The union of any _finite_set_ of closed sets is closed

  closed_Union_closed: THEOREM
               FORALL (FS:finite_set[closed_set]): closed?(Union(FS))

  % Apostol 3.35b (2) (equivalent to Apostol 3.8 (generalized))
  % The union of any _collection_ of closed sets is closed

  closed_Intersection_closed: THEOREM
               FORALL (XS:set[closed_set]): closed?(Intersection(XS))

  % Apostol 3.36a

  open_closed_difference: LEMMA FORALL (A:open_set,B:closed_set):
                                                       open?(difference(A,B))
  % Apostol 3.36b

  closed_open_difference: LEMMA FORALL (A:open_set,B:closed_set):
                                                       closed?(difference(B,A))

  % Apostol Theorem 3.33

  open_def: THEOREM subset?(S,X) AND subset?(A,S) IMPLIES
                  (open?(A) IFF (EXISTS B: subset?(B,S) AND open?(B) AND A = intersection(B,S)))

  END metric_spaces

quality71%

¤ 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.0.21Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.