%------------------------------------------------------------------------------
% Topological Bases

% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% The material presented here comes from Sutherland Chapter 3, Section 2
%
%     Version 1.0            1/11/06  Initial Version
%------------------------------------------------------------------------------

basis[T:TYPE]: THEORY

BEGIN

  IMPORTING topology_prelim[T]

  t:     VAR topology
  U,V,W: VAR setofsets[T]
  A:     VAR set[T]

  base?(t)(U):bool = subset?(U,t) AND
                     FORALL (A:(t)): EXISTS V: subset?(V,U) AND Union(V) = A
                                                                    % Def 3.2.1

  base?(t,U):bool = base?(t)(U)

  synthetic_base?(U):bool
   = (EXISTS V: subset?(V,U) AND Union(V) = fullset[T]) AND
     FORALL (B1,B2:(U)): (EXISTS V: subset?(V,U) AND
                                   Union(V) = intersection(B1,B2))  % Def 3.2.2

  synthetic_base: TYPE = (synthetic_base?)

  synthetic_base_is_setofsets: JUDGEMENT synthetic_base SUBTYPE_OF setofsets[T]

  B: VAR synthetic_base

  synthetic_generated_topology_set(B):setofsets[T]
    = {A | EXISTS V: subset?(V,B) AND Union(V) = A}

  synthetic_generated_def: LEMMA
    member(A,synthetic_generated_topology_set(B)) IFF
    EXISTS V: subset?(V,B) AND Union(V) = A

  synthetic_generated_alt_def: LEMMA
    member(A,synthetic_generated_topology_set(B)) IFF
    A = Union({x:(B) | subset?(x,A)})

  synthetic_generated_empty:
       LEMMA member(emptyset[T],synthetic_generated_topology_set(B))

  synthetic_generated_full:
       LEMMA member(fullset[T],synthetic_generated_topology_set(B))

  synthetic_generated_Union:
       LEMMA topology_Union?(synthetic_generated_topology_set(B))

  synthetic_generated_intersection:
       LEMMA topology_intersection?(synthetic_generated_topology_set(B))

  synthetic_generated_topology(B):topology
    = {A | EXISTS V: subset?(V,B) AND Union(V) = A}

  synthetic_basis_is_topology:
       JUDGEMENT synthetic_generated_topology_set(B) HAS_TYPE topology

  base_is_synthetic_base: LEMMA base?(t)(U) => synthetic_base?(U)

  synthetic_base_is_base:
       LEMMA base?(synthetic_generated_topology_set(B))(B)

  subbase?(t)(U):bool
   = subset?(U,t) AND
     base?(t)({A | EXISTS V: is_finite(V) AND subset?(V,U) AND
                             A = Intersection(V)})

  subbase?(t,U):bool = subbase?(t)(U)

  synthetic_subbase?(U):bool
   = synthetic_base?({A | EXISTS V: is_finite(V) AND subset?(V,U) AND
                                    A = Intersection(V)})

  synthetic_subbase: TYPE = (synthetic_subbase?)

  synthetic_subbase_is_setofsets:
                            JUDGEMENT synthetic_subbase SUBTYPE_OF setofsets[T]

  S: VAR synthetic_subbase

%  synthetic_base_is_synthetic_subbase:
%                         JUDGEMENT synthetic_base SUBTYPE_OF synthetic_subbase



END basis