products/sources/formale Sprachen/Coq/plugins/ssr image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: homeomorphic_symmetric.pvs   Sprache: Unknown

%------------------------------------------------------------------------------
% Homeomorphisms are Symmetric
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            8/7/04  Initial Version
%------------------------------------------------------------------------------

homeomorphic_symmetric[T1:TYPE, (IMPORTING topology_def[T1]) S:topology[T1],
                       T2:TYPE, (IMPORTING topology_def[T2]) T:topology[T2]
                      ]: THEORY

BEGIN

  IMPORTING homeomorphism_def,
            structures@function_inverse_alt_aux % For proof only

  homeomorphic_symmetric: LEMMA homeomorphic?[T1,S,T2,T](S,T) IFF
                                homeomorphic?[T2,T,T1,S](T,S)

END homeomorphic_symmetric

[ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ]