Quelle compactness.pvs Sprache: PVS

compactness[T:TYPE+,d:[T,T->nnreal]]: THEORY
%------------------------------------------------------------------------------
% Compactness
%
%     Authors: Anthony Narkawicz,  NASA Langley
%              Ricky Butler,       NASA Langley
%
%     Version 1.0         8/25/2009  Initial Version
%
%  Compactness proofs can be detailed and tricky.  It is highly recommended that
%  users of this library exploit the IdxCover mechanism developed here
%
%       Given a set H = { (a,r) } where a = center of a ball and
%                                       r = radius of a ball
%       for which
%
%            ball_covering(H) = { balls(a,r) | H(a,r) }
%
%       idxCover returns
%             N:  size of a finite covering
%             seq: below[N] -> (H)
%
%       which provides a finite sub-cover, i.e.
%
%           open_cover?(ball_covering({h: [T,posreal] | H(h)
%                       AND (EXISTS (n: below[N]): h = seq(n))}),S)
%
%------------------------------------------------------------------------------
BEGIN

   ASSUMING IMPORTING metric_spaces_def[T,d]
       fullset_metric_space: ASSUMPTION metric_space?[T,d](fullset[T])
   ENDASSUMING

  CONVERSION+ singleton

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

  IMPORTING metric_spaces[T,d]

  XS,YS: VAR set[set[T]]

  open_cover?(XS,S): bool = subset?(S,Union(XS)) AND
                            (FORALL (C: set[T]): XS(C) IMPLIES open?(C))


  finite_cover?(XS,S): bool  = is_finite(XS) AND open_cover?(XS,S)

  compact?(S): bool          = FORALL XS: open_cover?(XS,S) IMPLIES
                               EXISTS YS: subset?(YS,XS) & finite_cover?(YS,S)

  bounded?(S): bool          = EXISTS r: FORALL x,y: S(x) AND S(y) IMPLIES ball(x,r)(y)

  precompact?(S): bool       = FORALL r: EXISTS (X:set[T]):
                               finite_cover?({z:set[T] | EXISTS (x:(X)): ball(x,r) = z},S)

  nBalls(p:T): set[(open?)] = {s: set[T] | EXISTS (n: posnat): s = ball(p,n)}

  p: VAR T
  nBalls_open_cover: LEMMA open_cover?(nBalls(p),S)

  % Helpful Property Of Compact Sets

  H: VAR set[[T,posreal]]

  ball_covering(H): set[set[T]] = {s: set[T] | EXISTS (h: (H)): s = ball(h`1,h`2)}

  %exists_sequence: LEMMA

  reverse_ball(H: set[[T,posreal]],A: {s: (nonempty?[T]) | ball_covering(H)(s)}):
      {h: (H) | ball(h`1,h`2)  = A}

  set_compact: LEMMA
     (compact?(S) AND open_cover?(ball_covering(H),S))
     IMPLIES (EXISTS (N: nat, seq: [below[N] -> (H)]):
    open_cover?(ball_covering({h: [T,posreal] | H(h) AND
                                            (EXISTS (n: below[N]): h = seq(n))}),S))

% ----- Here is a mechanism to explicitly contruct a indexed finite subcover of any ---------------------
% ----- ball covering of a compact set

  Htype(S): TYPE = {H: set[[T,posreal]] | compact?(S) AND open_cover?(ball_covering(H),S)}

  idxCover(S: (compact?), H: Htype(S)):
      {pair: [N: nat,seq: [below[N]->(H)]] |
    open_cover?(ball_covering({h: [T,posreal] | H(h)
                 AND (EXISTS (n: below[pair`1]): h = pair`2(n))}),S)}
       = choose({ pair: [N: nat,seq: [below[N]->(H)]] |
              open_cover?(ball_covering({h: [T,posreal] | H(h)
                 AND (EXISTS (n: below[pair`1]): h = pair`2(n))}),S)})

  idxCover_def: LEMMA
      compact?(S) AND open_cover?(ball_covering(H),S) AND
      S(x) IMPLIES
            LET (N,seq) = idxCover(S,H) IN
              (EXISTS (n: below[N]): LET (a,r) = seq(n) IN
                   ball(a,r)(x) AND ball_covering(H)(ball(a,r)))

  set_compact_alt: LEMMA
      compact?(S) AND open_cover?(ball_covering(H),S)
      IMPLIES LET (N,seq) = idxCover(S,H) IN
         open_cover?(ball_covering({h: [T,posreal] | H(h) AND (EXISTS (n: below[N]): h = seq(n))}),S)

  N: var posint
  M:   var nat

  IMPORTING finite_sets@finite_sets_minmax[nat,<=]

  max_min_finite_scaf: LEMMA
      FORALL (P: [nat,below(N) -> bool]): (FORALL (n: below(N)):
         EXISTS (M: nat): FORALL (m: above(M)):
             P(m,n)) IMPLIES (EXISTS (TOTAL_M: nat): FORALL (m:above(TOTAL_M),n: below(N)): P(m,n))

  compact_sequence_limit: LEMMA
     (nonempty?(S) AND compact?(S))
      IMPLIES (FORALL (seq: [nat -> (S)]): EXISTS (p: (S)):
          FORALL (epsilon: posreal, N: posint): EXISTS (n: above(N)): d(seq(n),p) < epsilon)

  % Apostle Theorem 3.38
%%  compact_closed : LEMMA compact?(S) IMPLIES closed?(S)
%%  compact_bounded: LEMMA compact?(S) IMPLIES bounded?(S)

  compact_open_increasing_seq: LEMMA compact?(S) IMPLIES (FORALL (seq: [nat -> (open?)]): (FORALL (j: nat):
    subset?(seq(j),seq(j+1))) AND open_cover?({AZ: set[T] | EXISTS (k: nat): AZ = seq(k)},S) IMPLIES
    EXISTS (i: nat): subset?(S,seq(i)))

  closed_subset_of_compact: LEMMA compact?(S) AND subset?(W,S) AND closed?(W) IMPLIES compact?(W)

  compact_closed: LEMMA compact?(S) IMPLIES closed?(S)

  compact_bounded: LEMMA compact?(S) IMPLIES bounded?(S) % Added 09/2010

END compactness

quality76%

¤ Dauer der Verarbeitung: 0.13 Sekunden (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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.