The abstract of the Mizar article:

The Definition and Basic Properties of Topological Groups

by

Artur Kornilowicz

Received September 7, 1998

MML identifier: TOPGRP_1

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, SGRAPH1, FUNCT_1, RELAT_1, SUBSET_1, VECTSP_1, REALSET1,
      GROUP_1, ORDINAL2, TOPS_2, CONNSP_2, TOPS_1, BOOLE, FUNCT_2, BINOP_1,
      UNIALG_1, URYSOHN1, COMPTS_1, SETFAM_1, PCOMPS_1, TARSKI, TOPGRP_1,
      RLVECT_3, SEQ_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, TOPS_2, FUNCT_1,
      PARTFUN1, BINOP_1, SETFAM_1, GRCAT_1, REALSET1, GROUP_1, GROUP_2,
      STRUCT_0, VECTSP_1, PRE_TOPC, TOPS_1, COMPTS_1, PCOMPS_1, URYSOHN1,
      BORSUK_1, T_0TOPSP, CANTOR_1, FUNCT_2, YELLOW_8;
 constructors REALSET1, TOPS_1, TOPS_2, GRCAT_1, T_0TOPSP, GROUP_7, URYSOHN1,
      COMPTS_1, CANTOR_1, YELLOW_8, MEMBERED;
 clusters BORSUK_1, BORSUK_2, STRUCT_0, GROUP_1, PRE_TOPC, WAYBEL10, TEX_1,
      PCOMPS_1, TOPS_1, RELSET_1, SUBSET_1, FUNCT_2, PARTFUN1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin  :: Preliminaries

reserve S for 1-sorted,
        R for non empty 1-sorted,
        X for Subset of R,
        T for non empty TopStruct,
        x for set;

definition let X be set;
 cluster one-to-one onto Function of X, X;
end;

theorem :: TOPGRP_1:1
 rng id S = [#]S;

definition let R be non empty 1-sorted;
 cluster (id R)/" -> one-to-one;
end;

theorem :: TOPGRP_1:2
 (id R)/" = id R;

theorem :: TOPGRP_1:3
   (id R)"X = X;

definition let S be 1-sorted;
 cluster one-to-one onto map of S, S;
end;

begin  :: On the groups

reserve H for non empty HGrStr,
        P, Q, P1, Q1 for Subset of H,
        h for Element of H;

theorem :: TOPGRP_1:4
 P c= P1 & Q c= Q1 implies P * Q c= P1 * Q1;

theorem :: TOPGRP_1:5
 P c= Q implies P * h c= Q * h;

theorem :: TOPGRP_1:6
   P c= Q implies h * P c= h * Q;

reserve G for Group,
        A, B for Subset of G,
        a for Element of G;

theorem :: TOPGRP_1:7
  a in A" iff a" in A;

theorem :: TOPGRP_1:8
 A"" = A;

theorem :: TOPGRP_1:9
 A c= B iff A" c= B";

theorem :: TOPGRP_1:10
 (inverse_op G).:A = A";

theorem :: TOPGRP_1:11
 (inverse_op G)"A = A";

theorem :: TOPGRP_1:12
 inverse_op G is one-to-one;

theorem :: TOPGRP_1:13
 rng inverse_op G = the carrier of G;

definition let G be Group;
  cluster inverse_op G -> one-to-one onto;
end;

theorem :: TOPGRP_1:14
 (inverse_op G)" = inverse_op G;

theorem :: TOPGRP_1:15
 (the mult of H).:[:P,Q:] = P*Q;

definition let G be non empty HGrStr, a be Element of G;
 func a* -> map of G, G means
:: TOPGRP_1:def 1
  for x being Element of G holds it.x = a * x;
 func *a -> map of G, G means
:: TOPGRP_1:def 2
  for x being Element of G holds it.x = x * a;
end;

definition let G be Group, a be Element of G;
 cluster a* -> one-to-one onto;
 cluster *a -> one-to-one onto;
end;

theorem :: TOPGRP_1:16
 h*.:P = h * P;

theorem :: TOPGRP_1:17
 (*h).:P = P * h;

theorem :: TOPGRP_1:18
 a*/" = a"*;

theorem :: TOPGRP_1:19
 (*a)/" = *(a");

begin  :: On the topological spaces

definition let T be non empty TopStruct;
 cluster (id T)/" -> continuous;
end;

theorem :: TOPGRP_1:20
 id T is_homeomorphism;

definition let T be non empty TopSpace, p be Point of T;
 cluster -> non empty a_neighborhood of p;
end;

theorem :: TOPGRP_1:21
 for T being non empty TopSpace, p being Point of T holds
  [#]T is a_neighborhood of p;

definition let T be non empty TopSpace, p be Point of T;
 cluster non empty open a_neighborhood of p;
end;

theorem :: TOPGRP_1:22
   for S, T being non empty TopSpace, f being map of S, T st f is open holds
  for p being Point of S, P being a_neighborhood of p
   ex R being open a_neighborhood of f.p st R c= f.:P;

theorem :: TOPGRP_1:23
   for S, T being non empty TopSpace, f being map of S, T st
   for p being Point of S, P being open a_neighborhood of p
    ex R being a_neighborhood of f.p st R c= f.:P
  holds f is open;

theorem :: TOPGRP_1:24
   for S, T being non empty TopStruct, f being map of S, T holds
  f is_homeomorphism iff dom f = [#]S & rng f = [#]T & f is one-to-one &
   for P being Subset of T holds P is closed iff f"P is closed;

theorem :: TOPGRP_1:25
 for S, T being non empty TopStruct, f being map of S, T holds
  f is_homeomorphism iff dom f = [#]S & rng f = [#]T & f is one-to-one &
   for P being Subset of S holds P is open iff f.:P is open;

theorem :: TOPGRP_1:26
   for S, T being non empty TopStruct, f being map of S, T holds
  f is_homeomorphism iff dom f = [#]S & rng f = [#]T & f is one-to-one &
   for P being Subset of T holds P is open iff f"P is open;

theorem :: TOPGRP_1:27
   for S being TopSpace, T being non empty TopSpace, f being map of S, T holds
  f is continuous iff
  for P being Subset of T holds f"(Int P) c= Int(f"P);

definition let T be non empty TopSpace;
 cluster non empty dense Subset of T;
end;

theorem :: TOPGRP_1:28
 for S, T being non empty TopSpace, f being map of S, T,
     A being dense Subset of S st f is_homeomorphism
  holds f.:A is dense;

theorem :: TOPGRP_1:29
 for S, T being non empty TopSpace, f being map of S, T,
     A being dense Subset of T st f is_homeomorphism
  holds f"A is dense;

definition let S, T be non empty TopStruct;
 cluster being_homeomorphism -> onto one-to-one continuous open map of S, T;
end;

definition let T be non empty TopStruct;
 cluster being_homeomorphism map of T, T;
end;

definition let T be non empty TopStruct,
               f be being_homeomorphism map of T, T;
 cluster f/" -> being_homeomorphism;
end;

begin  :: The group of homoemorphisms

definition let T be non empty TopStruct;
 mode Homeomorphism of T -> map of T, T means
:: TOPGRP_1:def 3
  it is_homeomorphism;
end;

definition let T be non empty TopStruct;
 redefine func id T -> Homeomorphism of T;
end;

definition let T be non empty TopStruct;
 cluster -> being_homeomorphism Homeomorphism of T;
end;

theorem :: TOPGRP_1:30
 for f being Homeomorphism of T holds f/" is Homeomorphism of T;

theorem :: TOPGRP_1:31
 for f, g being Homeomorphism of T holds f * g is Homeomorphism of T;

definition let T be non empty TopStruct;
 func HomeoGroup T -> strict HGrStr means
:: TOPGRP_1:def 4
  (x in the carrier of it iff x is Homeomorphism of T) &
  for f, g being Homeomorphism of T holds (the mult of it).(f,g) = g * f;
end;

definition let T be non empty TopStruct;
 cluster HomeoGroup T -> non empty;
end;

theorem :: TOPGRP_1:32
   for f, g being Homeomorphism of T
  for a, b being Element of HomeoGroup T st f = a & g = b holds
   a * b = g * f;

definition let T be non empty TopStruct;
 cluster HomeoGroup T -> Group-like associative;
end;

theorem :: TOPGRP_1:33
 id T = 1.HomeoGroup T;

theorem :: TOPGRP_1:34
   for f being Homeomorphism of T
  for a being Element of HomeoGroup T st f = a holds a" = f/";

definition let T be non empty TopStruct;
 attr T is homogeneous means
:: TOPGRP_1:def 5
  for p, q being Point of T ex f being Homeomorphism of T st f.p = q;
end;

definition
 cluster trivial -> homogeneous (non empty TopStruct);
end;

definition
 cluster strict trivial non empty TopSpace;
end;

theorem :: TOPGRP_1:35
   for T being homogeneous (non empty TopSpace) st
  ex p being Point of T st {p} is closed holds T is_T1;

theorem :: TOPGRP_1:36
 for T being homogeneous (non empty TopSpace) st
  ex p being Point of T st for A being Subset of T st A is open & p in A holds
   ex B being Subset of T st p in B & B is open & Cl B c= A
  holds T is_T3;

begin  :: On the topological groups

definition
  struct (HGrStr, TopStruct) TopGrStr
     (# carrier -> set,
           mult -> BinOp of the carrier,
       topology -> Subset-Family of the carrier #);
end;

definition let A be non empty set,
               R be BinOp of A,
               T be Subset-Family of A;
 cluster TopGrStr (#A, R, T#) -> non empty;
end;

definition let x be set,
               R be BinOp of {x},
               T be Subset-Family of {x};
 cluster TopGrStr (#{x}, R, T#) -> trivial;
end;

definition
 cluster trivial -> Group-like associative commutative (non empty HGrStr);
end;

definition let a be set;
 cluster 1TopSp {a} -> trivial;
end;

definition
 cluster strict non empty TopGrStr;
end;

definition
 cluster strict TopSpace-like trivial (non empty TopGrStr);
end;

definition let G be Group-like associative (non empty TopGrStr);
 redefine func inverse_op G -> map of G, G;
end;

definition let G be Group-like associative (non empty TopGrStr);
 attr G is UnContinuous means
:: TOPGRP_1:def 6
  inverse_op G is continuous;
end;

definition let G be TopSpace-like TopGrStr;
 attr G is BinContinuous means
:: TOPGRP_1:def 7
  for f being map of [:G,G:], G st f = the mult of G holds f is continuous;
end;

definition
 cluster strict commutative trivial UnContinuous BinContinuous
         (TopSpace-like Group-like associative (non empty TopGrStr));
end;

definition
 mode TopGroup is TopSpace-like Group-like associative (non empty TopGrStr);
end;

definition
 mode TopologicalGroup is UnContinuous BinContinuous TopGroup;
end;

theorem :: TOPGRP_1:37
 for T being BinContinuous non empty (TopSpace-like TopGrStr),
     a, b being Element of T,
     W being a_neighborhood of a*b
  ex A being open a_neighborhood of a, B being open a_neighborhood of b st
   A*B c= W;

theorem :: TOPGRP_1:38
 for T being TopSpace-like non empty TopGrStr st
  (for a, b being Element of T,
       W being a_neighborhood of a*b
   ex A being a_neighborhood of a, B being a_neighborhood of b st A*B c= W)
  holds T is BinContinuous;

theorem :: TOPGRP_1:39
 for T being UnContinuous TopGroup,
     a being Element of T,
     W being a_neighborhood of a"
  ex A being open a_neighborhood of a st A" c= W;

theorem :: TOPGRP_1:40
 for T being TopGroup st
   for a being Element of T,
        W being a_neighborhood of a"
     ex A being a_neighborhood of a st A" c= W holds
  T is UnContinuous;

theorem :: TOPGRP_1:41
 for T being TopologicalGroup, a, b being Element of T
  for W being a_neighborhood of a*(b")
   ex A being open a_neighborhood of a, B being open a_neighborhood of b st
    A*(B") c= W;

theorem :: TOPGRP_1:42
   for T being TopGroup st
   for a, b being Element of T,
        W being a_neighborhood of a*(b")
    ex A being a_neighborhood of a, B being a_neighborhood of b st
     A*(B") c= W holds
  T is TopologicalGroup;

definition let G be BinContinuous non empty (TopSpace-like TopGrStr),
               a be Element of G;
 cluster a* -> continuous;
 cluster *a -> continuous;
end;

theorem :: TOPGRP_1:43
 for G being BinContinuous TopGroup,
     a being Element of G holds
   a* is Homeomorphism of G;

theorem :: TOPGRP_1:44
 for G being BinContinuous TopGroup,
     a being Element of G holds
  *a is Homeomorphism of G;

definition let G be BinContinuous TopGroup,
               a be Element of G;
 redefine func a* -> Homeomorphism of G;
 redefine func *a -> Homeomorphism of G;
end;

theorem :: TOPGRP_1:45
 for G being UnContinuous TopGroup holds inverse_op G is Homeomorphism of G;

definition let G be UnContinuous TopGroup;
 redefine func inverse_op G -> Homeomorphism of G;
end;

definition
 cluster BinContinuous -> homogeneous TopGroup;
end;

theorem :: TOPGRP_1:46
 for G being BinContinuous TopGroup, F being closed Subset of G,
     a being Element of G holds F * a is closed;

theorem :: TOPGRP_1:47
 for G being BinContinuous TopGroup, F being closed Subset of G,
     a being Element of G holds a * F is closed;

definition let G be BinContinuous TopGroup,
               F be closed Subset of G,
               a be Element of G;
 cluster F * a -> closed;
 cluster a * F -> closed;
end;

theorem :: TOPGRP_1:48
 for G being UnContinuous TopGroup, F being closed Subset of G
  holds F" is closed;

definition let G be UnContinuous TopGroup,
               F be closed Subset of G;
 cluster F" -> closed;
end;

theorem :: TOPGRP_1:49
 for G being BinContinuous TopGroup, O being open Subset of G,
     a being Element of G holds O * a is open;

theorem :: TOPGRP_1:50
 for G being BinContinuous TopGroup, O being open Subset of G,
     a being Element of G holds a * O is open;

definition let G be BinContinuous TopGroup,
               A be open Subset of G,
               a be Element of G;
 cluster A * a -> open;
 cluster a * A -> open;
end;

theorem :: TOPGRP_1:51
 for G being UnContinuous TopGroup, O being open Subset of G holds O" is open;

definition let G be UnContinuous TopGroup,
               A be open Subset of G;
 cluster A" -> open;
end;

theorem :: TOPGRP_1:52
 for G being BinContinuous TopGroup, A, O being Subset of G st O is open
  holds O * A is open;

theorem :: TOPGRP_1:53
 for G being BinContinuous TopGroup, A, O being Subset of G st O is open
  holds A * O is open;

definition let G be BinContinuous TopGroup,
               A be open Subset of G,
               B be Subset of G;
 cluster A * B -> open;
 cluster B * A -> open;
end;

theorem :: TOPGRP_1:54
 for G being UnContinuous TopGroup,
     a being Point of G, A being a_neighborhood of a
  holds A" is a_neighborhood of a";

theorem :: TOPGRP_1:55
 for G being TopologicalGroup, a being Point of G,
     A being a_neighborhood of a*a"
  ex B being open a_neighborhood of a st B*B" c= A;

theorem :: TOPGRP_1:56
 for G being UnContinuous TopGroup, A being dense Subset of G holds
  A" is dense;

definition let G be UnContinuous TopGroup,
               A be dense Subset of G;
 cluster A" -> dense;
end;

theorem :: TOPGRP_1:57
 for G being BinContinuous TopGroup, A being dense Subset of G,
     a being Point of G holds a*A is dense;

theorem :: TOPGRP_1:58
 for G being BinContinuous TopGroup, A being dense Subset of G,
     a being Point of G holds A*a is dense;

definition let G be BinContinuous TopGroup,
               A be dense Subset of G,
               a be Point of G;
 cluster A * a -> dense;
 cluster a * A -> dense;
end;

theorem :: TOPGRP_1:59
   for G being TopologicalGroup, B being Basis of 1.G, M being dense Subset of
G
  holds
{ V * x where V is Subset of G, x is Point of G: V in B & x in
 M }
  is Basis of G;

theorem :: TOPGRP_1:60
 for G being TopologicalGroup holds G is_T3;

definition
 cluster -> being_T3 TopologicalGroup;
end;