uniform3.miz
begin
reserve X for
set,
D for
a_partition of X,
TG for non
empty
TopologicalGroup;
reserve A for
Subset of X;
theorem ::
UNIFORM3:1
(
[:A, A:]
\/
[:(X
\ A), (X
\ A):])
c= (
[:(X
\ A), X:]
\/
[:X, A:])
proof
let x be
object;
assume x
in (
[:A, A:]
\/
[:(X
\ A), (X
\ A):]);
per cases by
XBOOLE_0:def 3;
suppose x
in
[:A, A:];
then
consider y,z be
object such that
A1: y
in A and
A2: z
in A and
A3: x
=
[y, z] by
ZFMISC_1:def 2;
x
in
[:(X
\ A), X:] or x
in
[:X, A:] by
A1,
A2,
A3,
ZFMISC_1: 87;
hence thesis by
XBOOLE_0:def 3;
end;
suppose x
in
[:(X
\ A), (X
\ A):];
then
consider y,z be
object such that
A4: y
in (X
\ A) and
A5: z
in (X
\ A) and
A6: x
=
[y, z] by
ZFMISC_1:def 2;
x
in
[:(X
\ A), X:] or x
in
[:X, A:] by
A4,
A5,
A6,
ZFMISC_1: 87;
hence thesis by
XBOOLE_0:def 3;
end;
end;
theorem ::
UNIFORM3:2
Th32: (
{1, 2, 3}
\
{1})
=
{2, 3}
proof
thus (
{1, 2, 3}
\
{1})
c=
{2, 3}
proof
let x be
object;
assume x
in (
{1, 2, 3}
\
{1});
then x
in
{1, 2, 3} & not x
in
{1} by
XBOOLE_0:def 5;
then (x
= 1 or x
= 2 or x
= 3) & not x
= 1 by
ENUMSET1:def 1,
TARSKI:def 1;
hence thesis by
TARSKI:def 2;
end;
let x be
object;
assume x
in
{2, 3};
then x
= 2 or x
= 3 by
TARSKI:def 2;
then x
in
{1, 2, 3} & not x
in
{1} by
ENUMSET1:def 1,
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 5;
end;
theorem ::
UNIFORM3:3
X
=
{1, 2, 3} & A
=
{1} implies
[2, 1]
in (
[:(X
\ A), X:]
\/
[:X, A:]) & not
[2, 1]
in (
[:A, A:]
\/
[:(X
\ A), (X
\ A):])
proof
assume that
A1: X
=
{1, 2, 3} and
A2: A
=
{1};
1
in X & 2
in (X
\ A) by
A1,
A2,
Th32,
TARSKI:def 2,
ENUMSET1:def 1;
then
[2, 1]
in
[:(X
\ A), X:] by
ZFMISC_1: 87;
hence
[2, 1]
in (
[:(X
\ A), X:]
\/
[:X, A:]) by
XBOOLE_0:def 3;
assume
[2, 1]
in (
[:A, A:]
\/
[:(X
\ A), (X
\ A):]);
then
[2, 1]
in
[:A, A:] or
[2, 1]
in
[:(X
\ A), (X
\ A):] by
XBOOLE_0:def 3;
then 2
in
{1} or 1
in
{2, 3} by
A1,
A2,
Th32,
ZFMISC_1: 87;
hence thesis by
TARSKI:def 1,
TARSKI:def 2;
end;
theorem ::
UNIFORM3:4
Th33: for A be
Subset of X holds ((
[:A, A:]
\/
[:(X
\ A), (X
\ A):])
~ )
= (
[:A, A:]
\/
[:(X
\ A), (X
\ A):])
proof
let A be
Subset of X;
(
[:A, A:]
~ )
=
[:A, A:] & (
[:(X
\ A), (X
\ A):]
~ )
=
[:(X
\ A), (X
\ A):] by
SYSREL: 5;
hence thesis by
RELAT_1: 23;
end;
Th1: for P1,P2 be
Subset of D st (
union P1)
= (
union P2) holds P1
c= P2
proof
let P1,P2 be
Subset of D;
assume
A1: (
union P1)
= (
union P2);
let x be
object;
assume
A2: x
in P1;
assume
A3: not x
in P2;
x
in D by
A2;
then
reconsider x as
Subset of X;
A4: x
<>
{} by
A2,
EQREL_1:def 4;
set a = the
Element of x;
a
in (
union P2) by
A1,
A2,
A4,
TARSKI:def 4;
then
consider y be
set such that
A5: a
in y and
A6: y
in P2 by
TARSKI:def 4;
A7: not x
misses y by
A4,
A5,
XBOOLE_0:def 4;
x
in D & y
in D by
A2,
A6;
hence thesis by
A3,
A6,
A7,
EQREL_1:def 4;
end;
theorem ::
UNIFORM3:5
for P1,P2 be
Subset of D st (
union P1)
= (
union P2) holds P1
= P2 by
Th1;
theorem ::
UNIFORM3:6
Th2: for P be
Subset of D holds (
union (D
\ P))
= ((
union D)
\ (
union P))
proof
let P be
Subset of D;
thus (
union (D
\ P))
c= ((
union D)
\ (
union P))
proof
let x be
object;
assume x
in (
union (D
\ P));
then
consider y be
set such that
A2: x
in y and
A3: y
in (D
\ P) by
TARSKI:def 4;
y
in D & not y
in P by
A3,
XBOOLE_0:def 5;
then
A4: x
in (
union D) by
A2,
TARSKI:def 4;
not x
in (
union P)
proof
assume x
in (
union P);
then
consider z be
set such that
A5: x
in z and
A6: z
in P by
TARSKI:def 4;
z
in D & y
in D by
A3,
A6,
XBOOLE_0:def 5;
then y
= z or y
misses z by
EQREL_1:def 4;
hence thesis by
A2,
A5,
A6,
A3,
XBOOLE_0:def 4,
XBOOLE_0:def 5;
end;
hence thesis by
A4,
XBOOLE_0:def 5;
end;
let x be
object;
assume x
in ((
union D)
\ (
union P));
then
A7: x
in (
union D) & not x
in (
union P) by
XBOOLE_0:def 5;
then
consider y be
set such that
A8: x
in y and
A9: y
in D by
TARSKI:def 4;
y
in (D
\ P)
proof
assume not y
in (D
\ P);
then y
in P or not y
in D by
XBOOLE_0:def 5;
hence thesis by
A7,
A8,
A9,
TARSKI:def 4;
end;
hence thesis by
A8,
TARSKI:def 4;
end;
theorem ::
UNIFORM3:7
for SF be
upper
Subset-Family of X, S be
Element of SF holds (
meet SF)
c= S
proof
let SF be
upper
Subset-Family of X, S be
Element of SF;
let x be
object;
assume
A1: x
in (
meet SF);
per cases ;
suppose SF is
empty;
hence thesis by
A1,
SETFAM_1:def 1;
end;
suppose SF is non
empty;
hence thesis by
A1,
SETFAM_1:def 1;
end;
end;
theorem ::
UNIFORM3:8
Th3: for G be
addGroup, A,B,C,D be
Subset of G st A
c= B & C
c= D holds (A
+ C)
c= (B
+ D)
proof
let G be
addGroup, A,B,C,D be
Subset of G;
assume that
A1: A
c= B and
A2: C
c= D;
let x be
object;
assume x
in (A
+ C);
then ex a,c be
Element of G st x
= (a
+ c) & a
in A & c
in C;
hence thesis by
A1,
A2;
end;
theorem ::
UNIFORM3:9
Th4: for e be
Element of TG, V be
a_neighborhood of (
1_ TG) holds (
{e}
* V) is
a_neighborhood of e
proof
let e be
Element of TG, V be
a_neighborhood of (
1_ TG);
consider o be
Subset of TG such that
A1: o is
open and
A2: o
c= V and
A3: (
1_ TG)
in o by
CONNSP_2: 6;
now
thus (e
* o) is
open by
A1;
thus (e
* o)
c= (
{e}
* V)
proof
let x be
object;
assume
A4: x
in (e
* o);
(e
* o)
c= (e
* V) by
A2,
GROUP_3: 5;
hence thesis by
A4;
end;
e
= (e
* (
1_ TG)) by
GROUP_1:def 4;
hence e
in (e
* o) by
A3,
GROUP_2: 27;
end;
hence thesis by
CONNSP_2: 6;
end;
theorem ::
UNIFORM3:10
Th5: for e be
Element of TG, V be
a_neighborhood of (
1_ TG) holds (V
*
{e}) is
a_neighborhood of e
proof
let e be
Element of TG, V be
a_neighborhood of (
1_ TG);
consider o be
Subset of TG such that
A1: o is
open and
A2: o
c= V and
A3: (
1_ TG)
in o by
CONNSP_2: 6;
now
thus (o
* e) is
open by
A1;
thus (o
* e)
c= (V
*
{e})
proof
let x be
object;
assume
A4: x
in (o
* e);
(o
* e)
c= (V
* e) by
A2,
GROUP_3: 5;
hence thesis by
A4;
end;
e
= ((
1_ TG)
* e) by
GROUP_1:def 4;
hence e
in (o
* e) by
A3,
GROUP_2: 28;
end;
hence thesis by
CONNSP_2: 6;
end;
theorem ::
UNIFORM3:11
for V be
a_neighborhood of (
1_ TG) holds (V
" ) is
a_neighborhood of (
1_ TG)
proof
let V be
a_neighborhood of (
1_ TG);
(V
" ) is
a_neighborhood of ((
1_ TG)
" ) by
TOPGRP_1: 54;
hence thesis by
GROUP_1: 8;
end;
begin
definition
mode
UniformSpace is
upper
cap-closed
axiom_U1
axiom_U2
axiom_U3
UniformSpaceStr;
end
reserve US for
UniformSpace;
theorem ::
UNIFORM3:12
US is
axiom_U2
Quasi-UniformSpace;
theorem ::
UNIFORM3:13
US is
axiom_U3
Semi-UniformSpace;
definition
let X be
set, cB be
Subset-Family of
[:X, X:];
::
UNIFORM3:def1
attr cB is
axiom_UP2 means for B1 be
Element of cB holds ex B2 be
Element of cB st B2
c= (B1
~ );
end
theorem ::
UNIFORM3:14
for X be
empty
set, cB be
empty
Subset-Family of
[:X, X:] holds cB is
quasi_basis & cB is
axiom_UP1 & cB is
axiom_UP2 & cB is
axiom_UP3
proof
let X be
empty
set, cB be
empty
Subset-Family of
[:X, X:];
for B1,B2 be
Element of cB holds ex B be
Element of cB st B
c= (B1
/\ B2)
proof
let B1,B2 be
Element of cB;
reconsider B =
{} as
Element of cB by
SUBSET_1:def 1;
take B;
thus thesis;
end;
hence cB is
quasi_basis;
for B be
Element of cB holds (
id X)
c= B;
hence cB is
axiom_UP1;
for B1 be
Element of cB holds ex B2 be
Element of cB st B2
c= (B1
~ )
proof
let B1 be
Element of cB;
reconsider B2 =
{} as
Element of cB by
SUBSET_1:def 1;
B2
c= (B1
~ );
hence thesis;
end;
hence cB is
axiom_UP2;
for B1 be
Element of cB holds ex B2 be
Element of cB st (B2
* B2)
c= B1
proof
let B1 be
Element of cB;
reconsider B2 =
{} as
Element of cB by
SUBSET_1:def 1;
(B2
* B2)
c= B1;
hence thesis;
end;
hence cB is
axiom_UP3;
end;
registration
cluster
strict for
UniformSpace;
existence
proof
reconsider SF =
{
{} } as
Subset-Family of
[:
{} ,
{} :] by
ZFMISC_1: 1;
set US =
UniformSpaceStr (#
{} , SF #);
now
the
entourages of US is
upper;
hence US is
upper;
the
entourages of US is
cap-closed;
hence US is
cap-closed;
for S be
Element of the
entourages of US holds (
id the
carrier of US)
c= S;
hence US is
axiom_U1;
now
let S be
Element of the
entourages of US;
(S
[~] )
=
{} ;
hence (S
~ )
in the
entourages of US by
TARSKI:def 1;
end;
hence US is
axiom_U2;
now
let S be
Element of the
entourages of US;
(S
[*] S)
=
{} ;
then (S
* S)
= S by
TARSKI:def 1;
hence ex W be
Element of the
entourages of US st (W
* W)
c= S;
end;
hence US is
axiom_U3;
end;
hence thesis;
end;
end
theorem ::
UNIFORM3:15
Th6: for X be
set, SF be
Subset-Family of
[:X, X:] st X
=
{
{} } & SF
=
{
[:X, X:]} holds
UniformSpaceStr (# X, SF #) is
UniformSpace
proof
set X =
{
{} };
reconsider SF =
{
[:X, X:]} as
Subset-Family of
[:X, X:] by
ZFMISC_1: 68;
set US =
UniformSpaceStr (# X, SF #);
now
for Y1,Y2 be
Subset of
[:the
carrier of US, the
carrier of US:] st Y1
in the
entourages of US & Y1
c= Y2 holds Y2
in the
entourages of US
proof
let Y1,Y2 be
Subset of
[:the
carrier of US, the
carrier of US:];
assume that
A1: Y1
in the
entourages of US and
A2: Y1
c= Y2;
A3: Y1
=
[:X, X:] by
A1,
TARSKI:def 1;
Y1
= Y2 by
A2,
A3;
hence thesis by
A1;
end;
then the
entourages of US is
upper;
hence US is
upper;
for a,b be
Subset of
[:the
carrier of US, the
carrier of US:] st a
in the
entourages of US & b
in the
entourages of US holds (a
/\ b)
in the
entourages of US
proof
let a,b be
Subset of
[:the
carrier of US, the
carrier of US:];
assume that
A4: a
in the
entourages of US and
A5: b
in the
entourages of US;
a
=
[:X, X:] & b
=
[:X, X:] by
A4,
A5,
TARSKI:def 1;
hence (a
/\ b)
in the
entourages of US by
TARSKI:def 1;
end;
hence US is
cap-closed by
ROUGHS_4:def 2;
for S be
Element of the
entourages of US holds (
id X)
c= S
proof
let S be
Element of the
entourages of US;
S
=
[:X, X:] by
TARSKI:def 1;
hence thesis;
end;
hence US is
axiom_U1;
for S be
Element of the
entourages of US holds (S
[~] )
in the
entourages of US
proof
let S be
Element of the
entourages of US;
S
=
[:X, X:] by
TARSKI:def 1;
then (S
[~] )
=
[:X, X:] by
SYSREL: 5;
hence thesis by
TARSKI:def 1;
end;
hence US is
axiom_U2;
for S be
Element of the
entourages of US holds ex W be
Element of the
entourages of US st (W
[*] W)
c= S
proof
let S be
Element of the
entourages of US;
take S;
S
=
[:X, X:] by
TARSKI:def 1;
hence thesis;
end;
hence US is
axiom_U3;
end;
hence thesis;
end;
registration
cluster non
empty for
strict
UniformSpace;
existence
proof
set X =
{
{} };
reconsider SF =
{
[:X, X:]} as
Subset-Family of
[:X, X:] by
ZFMISC_1: 68;
set US =
UniformSpaceStr (# X, SF #);
A1: US is non
empty;
US is
strict
UniformSpace by
Th6;
hence thesis by
A1;
end;
end
theorem ::
UNIFORM3:16
Th7: for X be
set, cB be
Subset-Family of
[:X, X:] st cB is
quasi_basis
axiom_UP1
axiom_UP2
axiom_UP3 holds ex US be
strict
UniformSpace st the
carrier of US
= X & the
entourages of US
=
<.cB.]
proof
let X be
set, cB be
Subset-Family of
[:X, X:];
assume that
A1: cB is
quasi_basis and
A2: cB is
axiom_UP1 and
A3: cB is
axiom_UP2 and
A4: cB is
axiom_UP3;
set US =
UniformSpaceStr (# X,
<.cB.] #);
A5:
<.cB.]
= { x where x be
Subset of
[:X, X:] : ex b be
Element of cB st b
c= x } by
CARDFIL2: 14;
now
for Y1,Y2 be
Subset of
[:X, X:] st Y1
in
<.cB.] & Y1
c= Y2 holds Y2
in
<.cB.]
proof
let Y1,Y2 be
Subset of
[:X, X:];
assume that
A6: Y1
in
<.cB.] and
A7: Y1
c= Y2;
consider x be
Subset of
[:X, X:] such that
A8: Y1
= x and
A9: ex b be
Element of cB st b
c= x by
A5,
A6;
consider B be
Element of cB such that
A10: B
c= x by
A9;
B
c= Y2 by
A10,
A8,
A7;
hence thesis by
A5;
end;
then
<.cB.] is
upper;
hence US is
upper;
for Y1,Y2 be
set st Y1
in
<.cB.] & Y2
in
<.cB.] holds (Y1
/\ Y2)
in
<.cB.]
proof
let Y1,Y2 be
set;
assume that
A11: Y1
in
<.cB.] and
A12: Y2
in
<.cB.];
consider x be
Subset of
[:X, X:] such that
A13: Y1
= x and
A14: ex b be
Element of cB st b
c= x by
A5,
A11;
consider B1 be
Element of cB such that
A15: B1
c= x by
A14;
Y2
in { x where x be
Subset of
[:X, X:] : ex b be
Element of cB st b
c= x } by
CARDFIL2: 14,
A12;
then
consider y be
Subset of
[:X, X:] such that
A16: Y2
= y and
A17: ex b be
Element of cB st b
c= y;
consider B2 be
Element of cB such that
A18: B2
c= y by
A17;
A19: (B1
/\ B2)
c= (Y1
/\ Y2) by
A13,
A15,
A18,
A16,
XBOOLE_1: 27;
consider B3 be
Element of cB such that
A20: B3
c= (B1
/\ B2) by
A1;
A21: (Y1
/\ Y2)
c= (
[:X, X:]
/\
[:X, X:]) by
A11,
A12,
XBOOLE_1: 27;
B3
c= (Y1
/\ Y2) by
A20,
A19;
hence thesis by
A5,
A21;
end;
hence US is
cap-closed by
FINSUB_1:def 2;
for S be
Element of
<.cB.] holds (
id X)
c= S
proof
let S be
Element of
<.cB.];
S
in { x where x be
Subset of
[:X, X:] : ex b be
Element of cB st b
c= x } by
A5;
then
consider x be
Subset of
[:X, X:] such that
A22: S
= x and
A23: ex b be
Element of cB st b
c= x;
consider B be
Element of cB such that
A24: B
c= x by
A23;
(
id X)
c= B by
A2;
hence thesis by
A24,
A22;
end;
hence US is
axiom_U1;
for S be
Element of
<.cB.] holds (S
~ )
in
<.cB.]
proof
let S be
Element of
<.cB.];
reconsider S1 = S as
Subset of
[:X, X:];
consider B be
Element of cB such that
A27: B
c= S1 by
CARDFIL2:def 8;
A29: (B
~ )
c= (S1
~ ) by
A27,
SYSREL: 11;
consider B2 be
Element of cB such that
A30: B2
c= (B
~ ) by
A3;
B2
c= (S1
~ ) by
A29,
A30;
hence thesis by
CARDFIL2:def 8;
end;
hence US is
axiom_U2;
for S be
Element of the
entourages of US holds ex W be
Element of the
entourages of US st (W
* W)
c= S
proof
let S be
Element of the
entourages of US;
S
in
<.cB.];
then
consider B1 be
Element of cB such that
A31: B1
c= S by
CARDFIL2:def 8;
consider B2 be
Element of cB such that
A32: (B2
* B2)
c= B1 by
A4;
per cases ;
suppose
A34: cB is
empty;
then
A35: B2
=
{} by
SUBSET_1:def 1;
{}
c=
[:X, X:];
then
reconsider B2 as
Element of the
entourages of US by
A35,
A34,
CARDFIL2: 15;
(B2
[*] B2)
c= S by
A35;
hence thesis;
end;
suppose
A36: cB is non
empty;
cB
c=
<.cB.] by
CARDFIL2: 18;
then
reconsider W = B2 as
Element of the
entourages of US by
A36;
(W
[*] W)
c= S by
A31,
A32;
hence thesis;
end;
end;
hence US is
axiom_U3;
end;
then
reconsider US as
strict
UniformSpace;
take US;
thus the
carrier of US
= X;
thus the
entourages of US
=
<.cB.];
end;
begin
theorem ::
UNIFORM3:17
for US be non
empty
UniformSpace holds the
carrier of (
TopSpace_induced_by US)
= the
carrier of US & the
topology of (
TopSpace_induced_by US)
= (
Family_open_set (
FMT_induced_by US)) by
FINTOPO7:def 16;
theorem ::
UNIFORM3:18
Th8: for US be non
empty
UniformSpace, S be
Subset of (
FMT_induced_by US) holds S is
open iff for x be
Element of US st x
in S holds S
in (
Neighborhood x)
proof
let US be non
empty
UniformSpace, S be
Subset of (
FMT_induced_by US);
hereby
assume
A1: S is
open;
hereby
let x be
Element of US;
assume
A2: x
in S;
reconsider x1 = x as
Element of (
FMT_induced_by US);
(
U_FMT x1)
= (
Neighborhood x) by
UNIFORM2:def 14;
hence S
in (
Neighborhood x) by
A1,
A2;
end;
end;
assume
A3: for x be
Element of US st x
in S holds S
in (
Neighborhood x);
now
let x be
Element of (
FMT_induced_by US);
assume
A4: x
in S;
consider y be
Element of US such that
A5: x
= y and
A6: (
U_FMT x)
= ((
Neighborhood US)
. y);
(
U_FMT x)
= (
Neighborhood y) by
A6,
UNIFORM2:def 14;
hence S
in (
U_FMT x) by
A3,
A4,
A5;
end;
hence S is
open;
end;
theorem ::
UNIFORM3:19
for US be non
empty
UniformSpace holds (
Family_open_set (
FMT_induced_by US))
= the set of all O where O be
open
Subset of (
FMT_induced_by US);
theorem ::
UNIFORM3:20
Th9: for US be non
empty
UniformSpace, S be
Subset of (
FMT_induced_by US) holds S is
open iff S
in (
Family_open_set (
FMT_induced_by US))
proof
let US be non
empty
UniformSpace, S be
Subset of (
FMT_induced_by US);
thus S is
open implies S
in (
Family_open_set (
FMT_induced_by US));
assume S
in (
Family_open_set (
FMT_induced_by US));
then ex O be
open
Subset of (
FMT_induced_by US) st S
= O;
hence S is
open;
end;
theorem ::
UNIFORM3:21
for US be non
empty
UniformSpace, S be
Subset of (
FMT_induced_by US) holds S
in (
Family_open_set (
FMT_induced_by US)) iff for x be
Element of US st x
in S holds S
in (
Neighborhood x) by
Th8,
Th9;
begin
definition
let MS be non
empty
MetrStruct, r be
positive
Real;
::
UNIFORM3:def2
func
fundamental_element_of_entourages (MS,r) ->
Subset of
[:the
carrier of MS, the
carrier of MS:] equals {
[x, y] where x,y be
Element of MS : (
dist (x,y))
<= r };
coherence
proof
set S = {
[x, y] where x,y be
Element of MS : (
dist (x,y))
<= r };
S
c=
[:the
carrier of MS, the
carrier of MS:]
proof
let t be
object;
assume t
in S;
then ex x,y be
Element of MS st t
=
[x, y] & (
dist (x,y))
<= r;
hence thesis;
end;
hence thesis;
end;
end
registration
let MS be non
empty
Reflexive
MetrStruct, r be
positive
Real;
cluster (
fundamental_element_of_entourages (MS,r)) -> non
empty;
coherence
proof
the
carrier of MS is non
empty;
then
consider s be
object such that
A1: s
in the
carrier of MS;
reconsider s as
Element of MS by
A1;
(
dist (s,s))
=
0 by
METRIC_1: 1;
then
[s, s]
in (
fundamental_element_of_entourages (MS,r));
hence thesis;
end;
end
definition
let MS be non
empty
MetrStruct;
::
UNIFORM3:def3
func
fundamental_system_of_entourages (MS) -> non
empty
Subset-Family of
[:the
carrier of MS, the
carrier of MS:] equals the set of all (
fundamental_element_of_entourages (MS,r)) where r be
positive
Real;
coherence
proof
set SF = the set of all (
fundamental_element_of_entourages (MS,r)) where r be
positive
Real;
SF
c= (
bool
[:the
carrier of MS, the
carrier of MS:])
proof
let t be
object;
assume t
in SF;
then
consider r be
positive
Real such that
A1: t
= (
fundamental_element_of_entourages (MS,r));
reconsider t1 = t as
Subset of
[:the
carrier of MS, the
carrier of MS:] by
A1;
t1
c=
[:the
carrier of MS, the
carrier of MS:];
hence thesis;
end;
then
reconsider SF as
Subset-Family of
[:the
carrier of MS, the
carrier of MS:];
(
fundamental_element_of_entourages (MS,1))
in SF;
hence thesis;
end;
end
definition
let MS be non
empty
MetrStruct;
::
UNIFORM3:def4
func
uniformity_induced_by MS ->
UniformSpaceStr equals
UniformSpaceStr (# the
carrier of MS,
<.(
fundamental_system_of_entourages MS).] #);
coherence ;
end
Th10: for MS be
PseudoMetricSpace holds ex US be
strict
UniformSpace st US
= (
uniformity_induced_by MS)
proof
let MS be
PseudoMetricSpace;
set US = (
uniformity_induced_by MS);
set cB = (
fundamental_system_of_entourages MS);
now
now
let B1,B2 be
Element of cB;
B1
in the set of all (
fundamental_element_of_entourages (MS,r)) where r be
positive
Real;
then
consider r1 be
positive
Real such that
A1: B1
= (
fundamental_element_of_entourages (MS,r1));
B2
in the set of all (
fundamental_element_of_entourages (MS,r)) where r be
positive
Real;
then
consider r2 be
positive
Real such that
A2: B2
= (
fundamental_element_of_entourages (MS,r2));
reconsider r3 = (
min (r1,r2)) as
positive
Real by
XXREAL_0:def 9;
set B3 = {
[x, y] where x,y be
Element of MS : (
dist (x,y))
<= r3 };
B3
= (
fundamental_element_of_entourages (MS,r3));
then B3
in the set of all (
fundamental_element_of_entourages (MS,r)) where r be
positive
Real;
then
reconsider B3 = {
[x, y] where x,y be
Element of the
carrier of MS : (
dist (x,y))
<= r3 } as
Element of cB;
B3
c= (B1
/\ B2)
proof
let t be
object;
assume t
in B3;
then
consider x,y be
Element of MS such that
A3: t
=
[x, y] and
A4: (
dist (x,y))
<= r3;
r3
<= r1 by
XXREAL_0: 17;
then (
dist (x,y))
<= r1 by
A4,
XXREAL_0: 2;
then
A5: t
in B1 by
A1,
A3;
r3
<= r2 by
XXREAL_0: 17;
then (
dist (x,y))
<= r2 by
A4,
XXREAL_0: 2;
then t
in B2 by
A3,
A2;
hence thesis by
A5,
XBOOLE_0:def 4;
end;
hence ex B be
Element of cB st B
c= (B1
/\ B2);
end;
hence cB is
quasi_basis;
now
let B be
Element of cB;
B
in the set of all (
fundamental_element_of_entourages (MS,r)) where r be
positive
Real;
then
consider r be
positive
Real such that
A6: B
= (
fundamental_element_of_entourages (MS,r));
now
let t be
object;
assume
A7: t
in (
id the
carrier of MS);
then
consider t1,t2 be
object such that
A8: t
=
[t1, t2] by
RELAT_1:def 1;
A9: t1
in the
carrier of MS & t1
= t2 by
A7,
A8,
RELAT_1:def 10;
then
reconsider t1, t2 as
Element of MS;
(
dist (t1,t1))
<= r by
METRIC_1: 1;
hence t
in B by
A9,
A8,
A6;
end;
hence (
id the
carrier of MS)
c= B;
end;
hence cB is
axiom_UP1;
now
let B1 be
Element of cB;
B1
in the set of all (
fundamental_element_of_entourages (MS,r)) where r be
positive
Real;
then
consider r be
positive
Real such that
A10: B1
= (
fundamental_element_of_entourages (MS,r));
B1
c= (B1
~ )
proof
let t be
object;
assume
A11: t
in B1;
then
consider x,y be
Element of MS such that
A12: t
=
[x, y] and (
dist (x,y))
<= r by
A10;
reconsider R1 = B1 as
Relation of the
carrier of MS;
A13: (R1
~ )
= {
[y, x] where x,y be
Element of MS : (
dist (x,y))
<= r }
proof
{
[y, x] where x,y be
Element of MS : (
dist (x,y))
<= r }
c=
[:the
carrier of MS, the
carrier of MS:]
proof
let u be
object;
assume u
in {
[y, x] where x,y be
Element of MS : (
dist (x,y))
<= r };
then ex u1,u2 be
Element of MS st u
=
[u2, u1] & (
dist (u1,u2))
<= r;
hence thesis;
end;
then
reconsider R2 = {
[y, x] where x,y be
Element of the
carrier of MS : (
dist (x,y))
<= r } as
Relation;
A14: (R1
~ )
c= R2
proof
let u be
object;
assume
A15: u
in (R1
~ );
consider u1,u2 be
object such that
A16: u
=
[u1, u2] by
A15,
RELAT_1:def 1;
[u2, u1]
in R1 by
A15,
A16,
RELAT_1:def 7;
then
consider v1,v2 be
Element of MS such that
A17:
[u2, u1]
=
[v1, v2] and
A18: (
dist (v1,v2))
<= r by
A10;
u2
= v1 & u1
= v2 by
A17,
XTUPLE_0: 1;
hence thesis by
A16,
A18;
end;
R2
c= (R1
~ )
proof
let u be
object;
assume
A19: u
in R2;
then
consider u1,u2 be
object such that
A20: u
=
[u1, u2] by
RELAT_1:def 1;
consider v1,v2 be
Element of MS such that
A21:
[u1, u2]
=
[v2, v1] and
A22: (
dist (v1,v2))
<= r by
A19,
A20;
[v1, v2]
in R1 by
A10,
A22;
hence thesis by
A20,
A21,
RELAT_1:def 7;
end;
hence thesis by
A14;
end;
consider x1,y1 be
Element of MS such that
A23:
[x, y]
=
[x1, y1] and
A24: (
dist (x1,y1))
<= r by
A10,
A11,
A12;
thus thesis by
A24,
A13,
A12,
A23;
end;
hence ex B2 be
Element of cB st B2
c= (B1
~ );
end;
hence cB is
axiom_UP2;
now
let B1 be
Element of cB;
B1
in the set of all (
fundamental_element_of_entourages (MS,r)) where r be
positive
Real;
then
consider r be
positive
Real such that
A25: B1
= (
fundamental_element_of_entourages (MS,r));
set B2 = {
[x, y] where x,y be
Element of MS : (
dist (x,y))
<= (r
/ 2) };
reconsider r2 = (r
/ 2) as
positive
Real;
B2
= (
fundamental_element_of_entourages (MS,r2));
then B2
in cB;
then
reconsider B2 as
Element of cB;
reconsider R1 = B2 as
Relation of the
carrier of MS;
(B2
* B2)
c= B1
proof
let t be
object;
assume t
in (B2
* B2);
then t
in {
[x, y] where x,y be
Element of MS : ex z be
Element of MS st
[x, z]
in R1 &
[z, y]
in R1 } by
UNIFORM2: 3;
then
consider x,y be
Element of MS such that
A29: t
=
[x, y] and
A30: ex z be
Element of MS st
[x, z]
in R1 &
[z, y]
in R1;
consider z be
Element of MS such that
A31:
[x, z]
in R1 and
A32:
[z, y]
in R1 by
A30;
consider x1,z1 be
Element of MS such that
A33:
[x, z]
=
[x1, z1] and
A34: (
dist (x1,z1))
<= (r
/ 2) by
A31;
A35: x
= x1 & z
= z1 by
A33,
XTUPLE_0: 1;
consider z1,y1 be
Element of MS such that
A36:
[z, y]
=
[z1, y1] and
A37: (
dist (z1,y1))
<= (r
/ 2) by
A32;
A38: z
= z1 & y
= y1 by
A36,
XTUPLE_0: 1;
A39: (
dist (x,y))
<= ((
dist (x,z))
+ (
dist (z,y))) by
METRIC_1: 4;
A40: ((
dist (x,z))
+ (
dist (z,y)))
<= ((
dist (x,z))
+ (r
/ 2)) by
A38,
A37,
XREAL_1: 6;
((
dist (x,z))
+ (r
/ 2))
<= ((r
/ 2)
+ (r
/ 2)) by
A35,
A34,
XREAL_1: 6;
then ((
dist (x,z))
+ (
dist (z,y)))
<= r by
A40,
XXREAL_0: 2;
then (
dist (x,y))
<= r by
A39,
XXREAL_0: 2;
hence thesis by
A29,
A25;
end;
hence ex B2 be
Element of cB st (B2
* B2)
c= B1;
end;
hence cB is
axiom_UP3;
end;
then ex US be
strict
UniformSpace st the
carrier of US
= the
carrier of MS & the
entourages of US
=
<.cB.] by
Th7;
hence thesis;
end;
definition
let MS be
PseudoMetricSpace;
::
UNIFORM3:def5
func
uniformity_induced_by (MS) -> non
empty
strict
UniformSpace equals
UniformSpaceStr (# the
carrier of MS,
<.(
fundamental_system_of_entourages MS).] #);
coherence
proof
ex US be
strict
UniformSpace st US
= (
uniformity_induced_by MS) by
Th10;
hence thesis;
end;
end
theorem ::
UNIFORM3:22
Th11: for MS be
PseudoMetricSpace holds (
Family_open_set (
FMT_induced_by (
uniformity_induced_by MS)))
= (
Family_open_set MS)
proof
let MS be
PseudoMetricSpace;
set X = (
Family_open_set (
FMT_induced_by (
uniformity_induced_by MS))), Y = (
Family_open_set MS);
thus X
c= Y
proof
let t be
object;
assume
A2: t
in X;
then
reconsider t1 = t as
Subset of (
FMT_induced_by (
uniformity_induced_by MS));
for x be
Point of MS st x
in t1 holds ex r be
Real st r
>
0 & (
Ball (x,r))
c= t1
proof
let x be
Point of MS;
assume
A3: x
in t1;
reconsider x1 = x as
Element of (
uniformity_induced_by MS);
t1
in (
Neighborhood x1) by
A3,
A2,
Th8,
Th9;
then
consider V0 be
Element of the
entourages of (
uniformity_induced_by MS) such that
A4: t1
= (
Neighborhood (V0,x1));
consider b be
Element of (
fundamental_system_of_entourages MS) such that
A5: b
c= V0 by
CARDFIL2:def 8;
b
in the set of all (
fundamental_element_of_entourages (MS,r)) where r be
positive
Real;
then
consider r0 be
positive
Real such that
A6: b
= (
fundamental_element_of_entourages (MS,r0));
now
take r0;
thus r0
>
0 ;
thus (
Ball (x,r0))
c= t1
proof
let u be
object;
assume
A7: u
in (
Ball (x,r0));
then
reconsider u1 = u as
Element of MS;
(
dist (x,u1))
< r0 by
A7,
METRIC_1: 11;
then
[x, u1]
in b by
A6;
hence thesis by
A4,
A5;
end;
end;
hence thesis;
end;
hence thesis by
PCOMPS_1:def 4;
end;
let t be
object;
assume
A8: t
in Y;
then
reconsider t1 = t as
Subset of MS;
for x be
Element of (
uniformity_induced_by MS) st x
in t1 holds t1
in (
Neighborhood x)
proof
let x be
Element of (
uniformity_induced_by MS);
assume
A9: x
in t1;
reconsider x1 = x as
Element of MS;
consider r0 be
Real such that
A10: r0
>
0 and
A11: (
Ball (x1,r0))
c= t1 by
A8,
PCOMPS_1:def 4,
A9;
reconsider r1 = (r0
/ 2) as
positive
Real by
A10;
set V0 = (
fundamental_element_of_entourages (MS,r1));
V0
in (
fundamental_system_of_entourages MS);
then
reconsider V0 as
Element of (
fundamental_system_of_entourages MS);
reconsider V1 = (V0
\/
[:t1, t1:]) as
Subset of
[:the
carrier of MS, the
carrier of MS:];
V0
c= V1 by
XBOOLE_1: 7;
then
reconsider V1 as
Element of the
entourages of (
uniformity_induced_by MS) by
CARDFIL2:def 8;
set Z = { y where y be
Element of (
uniformity_induced_by MS) :
[x, y]
in V1 };
Z
= t1
proof
thus Z
c= t1
proof
let u be
object;
assume u
in Z;
then
consider y0 be
Element of (
uniformity_induced_by MS) such that
A13: u
= y0 and
A14:
[x, y0]
in V1;
per cases by
A14,
XBOOLE_0:def 3;
suppose
[x, y0]
in V0;
then
consider x2,y2 be
Element of MS such that
A15:
[x, y0]
=
[x2, y2] and
A16: (
dist (x2,y2))
<= r1;
(r0
/ 2)
< (r0
/ 1) by
A10,
XREAL_1: 76;
then
A17: (
dist (x2,y2))
< r0 by
A16,
XXREAL_0: 2;
(
Ball (x2,r0))
= (
Ball (x1,r0)) by
A15,
XTUPLE_0: 1;
then y2
in t1 by
A17,
METRIC_1: 11,
A11;
hence thesis by
A13,
A15,
XTUPLE_0: 1;
end;
suppose
[x, y0]
in
[:t1, t1:];
then ex a,b be
object st a
in t1 & b
in t1 &
[x, y0]
=
[a, b] by
ZFMISC_1:def 2;
hence thesis by
A13,
XTUPLE_0: 1;
end;
end;
let v be
object;
assume
A18: v
in t1;
then
reconsider v1 = v as
Element of (
uniformity_induced_by MS);
[x, v1]
in
[:t1, t1:] by
A18,
A9,
ZFMISC_1:def 2;
then
[x, v1]
in V1 by
XBOOLE_0:def 3;
hence thesis;
end;
then t1
= (
Neighborhood (V1,x));
hence thesis;
end;
hence thesis by
Th8,
Th9;
end;
theorem ::
UNIFORM3:23
for MS be
PseudoMetricSpace holds (
TopSpace_induced_by (
uniformity_induced_by MS))
= (
TopSpaceMetr MS)
proof
let MS be
PseudoMetricSpace;
the
topology of (
FMT2TopSpace (
FMT_induced_by (
uniformity_induced_by MS)))
= (
Family_open_set (
FMT_induced_by (
uniformity_induced_by MS))) by
FINTOPO7:def 16;
hence thesis by
FINTOPO7:def 16,
Th11;
end;
begin
definition
let G be
TopologicalGroup;
let U be
a_neighborhood of (
1_ G);
::
UNIFORM3:def6
func
element_left_uniformity (U) ->
Subset of
[:the
carrier of G, the
carrier of G:] equals {
[x, y] where x be
Element of G, y be
Element of G : ((x
" )
* y)
in U };
coherence
proof
set S = {
[x, y] where x be
Element of G, y be
Element of G : ((x
" )
* y)
in U };
S
c=
[:the
carrier of G, the
carrier of G:]
proof
let t be
object;
assume t
in S;
then ex x,y be
Element of G st t
=
[x, y] & ((x
" )
* y)
in U;
hence thesis;
end;
hence thesis;
end;
end
definition
let TG be non
empty
TopologicalGroup;
::
UNIFORM3:def7
func
system_left_uniformity (TG) -> non
empty
Subset-Family of
[:the
carrier of TG, the
carrier of TG:] equals the set of all (
element_left_uniformity U) where U be
a_neighborhood of (
1_ TG);
coherence
proof
set SF = the set of all (
element_left_uniformity U) where U be
a_neighborhood of (
1_ TG);
reconsider nG = (
[#] TG) as
a_neighborhood of (
1_ TG) by
TOPGRP_1: 21;
A1: (
element_left_uniformity nG)
in SF;
SF
c= (
bool
[:the
carrier of TG, the
carrier of TG:])
proof
let t be
object;
assume t
in SF;
then ex U be
a_neighborhood of (
1_ TG) st t
= (
element_left_uniformity U);
hence thesis;
end;
hence thesis by
A1;
end;
end
definition
let TG be non
empty
TopologicalGroup;
::
UNIFORM3:def8
func
left_uniformity (TG) -> non
empty
UniformSpace equals
UniformSpaceStr (# the
carrier of TG,
<.(
system_left_uniformity TG).] #);
coherence
proof
set cB = (
system_left_uniformity TG);
now
now
let B1,B2 be
Element of cB;
B1
in (
system_left_uniformity TG);
then
consider U1 be
a_neighborhood of (
1_ TG) such that
A1: B1
= (
element_left_uniformity U1);
B2
in (
system_left_uniformity TG);
then
consider U2 be
a_neighborhood of (
1_ TG) such that
A2: B2
= (
element_left_uniformity U2);
reconsider U3 = (U1
/\ U2) as
a_neighborhood of (
1_ TG) by
CONNSP_2: 2;
set B3 = (
element_left_uniformity U3);
B3
in cB;
then
reconsider B3 as
Element of cB;
B3
c= (B1
/\ B2)
proof
let t be
object;
assume t
in B3;
then
consider x,y be
Element of TG such that
A3: t
=
[x, y] and
A4: ((x
" )
* y)
in U3;
((x
" )
* y)
in U1 & ((x
" )
* y)
in U2 by
A4,
XBOOLE_0:def 4;
then t
in B1 & t
in B2 by
A3,
A1,
A2;
hence thesis by
XBOOLE_0:def 4;
end;
hence ex B3 be
Element of cB st B3
c= (B1
/\ B2);
end;
hence cB is
quasi_basis;
now
let B be
Element of cB;
B
in (
system_left_uniformity TG);
then
consider U be
a_neighborhood of (
1_ TG) such that
A5: B
= (
element_left_uniformity U);
now
let t be
object;
assume
A6: t
in (
id the
carrier of TG);
then
consider x,y be
object such that
A7: x
in the
carrier of TG and
A8: y
in the
carrier of TG and
A9: t
=
[x, y] by
ZFMISC_1:def 2;
reconsider x, y as
Element of TG by
A7,
A8;
x
= y by
A6,
A9,
RELAT_1:def 10;
then ((x
" )
* y)
= (
1_ TG) by
GROUP_1:def 5;
then x is
Element of TG & y is
Element of TG & ((x
" )
* y)
in U by
CONNSP_2: 4;
hence t
in B by
A5,
A9;
end;
hence (
id the
carrier of TG)
c= B;
end;
hence cB is
axiom_UP1;
now
let B1 be
Element of cB;
B1
in (
system_left_uniformity TG);
then
consider U be
a_neighborhood of (
1_ TG) such that
A10: B1
= (
element_left_uniformity U);
consider R1 be
Relation of the
carrier of TG such that
A11: B1
= R1 and
A12: (R1
~ )
= (B1
~ );
(U
" ) is
a_neighborhood of ((
1_ TG)
" ) by
TOPGRP_1: 54;
then
reconsider U2 = (U
" ) as
a_neighborhood of (
1_ TG) by
GROUP_1: 8;
set B2 = (
element_left_uniformity U2);
B2
in cB;
then
reconsider B2 as
Element of cB;
B2
c= (B1
~ )
proof
let t be
object;
assume t
in B2;
then
consider a,b be
Element of TG such that
A13: t
=
[a, b] and
A14: ((a
" )
* b)
in U2;
consider g be
Element of TG such that
A15: ((a
" )
* b)
= (g
" ) and
A16: g
in U by
A14;
(((a
" )
* b)
" )
in U by
A15,
A16;
then ((b
" )
* ((a
" )
" ))
in U by
GROUP_1: 17;
then
[b, a]
in R1 by
A10,
A11;
hence thesis by
A12,
A13,
RELAT_1:def 7;
end;
hence ex B2 be
Element of cB st B2
c= (B1
~ );
end;
hence cB is
axiom_UP2;
now
let B1 be
Element of cB;
B1
in (
system_left_uniformity TG);
then
consider U be
a_neighborhood of (
1_ TG) such that
A17: B1
= (
element_left_uniformity U);
U is
a_neighborhood of ((
1_ TG)
* (
1_ TG)) by
GROUP_1:def 4;
then
consider A be
open
a_neighborhood of (
1_ TG), B be
open
a_neighborhood of (
1_ TG) such that
A17bis: (A
* B)
c= U by
TOPGRP_1: 37;
reconsider AB = (A
/\ B) as
a_neighborhood of (
1_ TG) by
CONNSP_2: 2;
AB
c= A & AB
c= B by
XBOOLE_1: 17;
then
A18: (AB
* AB)
c= (A
* B) by
GROUP_3: 4;
set B2 = (
element_left_uniformity AB);
B2
in cB;
then
reconsider B2 as
Element of cB;
(B2
* B2)
c= B1
proof
let t be
object;
assume
A19: t
in (B2
* B2);
reconsider R1 = B2 as
Relation of the
carrier of TG;
t
in {
[x, y] where x,y be
Element of TG : ex z be
Element of TG st
[x, z]
in R1 &
[z, y]
in R1 } by
A19,
UNIFORM2: 3;
then
consider x,y be
Element of TG such that
A23: t
=
[x, y] and
A24: ex z be
Element of TG st
[x, z]
in R1 &
[z, y]
in R1;
consider z be
Element of TG such that
A25:
[x, z]
in R1 and
A26:
[z, y]
in R1 by
A24;
consider a,b be
Element of TG such that
A27:
[x, z]
=
[a, b] and
A28: ((a
" )
* b)
in AB by
A25;
A29: x
= a & z
= b by
A27,
XTUPLE_0: 1;
consider c,d be
Element of TG such that
A30:
[z, y]
=
[c, d] and
A31: ((c
" )
* d)
in AB by
A26;
A32: z
= c & y
= d by
A30,
XTUPLE_0: 1;
A33: (((a
" )
* b)
* ((c
" )
* d))
= ((x
" )
* (z
* ((z
" )
* y))) by
A29,
A32,
GROUP_1:def 3
.= ((x
" )
* ((z
* (z
" ))
* y)) by
GROUP_1:def 3
.= ((x
" )
* ((
1_ TG)
* y)) by
GROUP_1:def 5
.= ((x
" )
* y) by
GROUP_1:def 4;
(((a
" )
* b)
* ((c
" )
* d))
in (AB
* AB) by
A31,
A28;
then ((x
" )
* y)
in U by
A18,
A33,
A17bis;
hence t
in B1 by
A17,
A23;
end;
hence ex B2 be
Element of cB st (B2
* B2)
c= B1;
end;
hence cB is
axiom_UP3;
end;
then ex US be
strict
UniformSpace st the
carrier of US
= the
carrier of TG & the
entourages of US
=
<.cB.] by
Th7;
hence thesis;
end;
end
definition
let G be
TopologicalGroup;
let U be
a_neighborhood of (
1_ G);
::
UNIFORM3:def9
func
element_right_uniformity (U) ->
Subset of
[:the
carrier of G, the
carrier of G:] equals {
[x, y] where x be
Element of G, y be
Element of G : (y
* (x
" ))
in U };
coherence
proof
set S = {
[x, y] where x be
Element of G, y be
Element of G : (y
* (x
" ))
in U };
S
c=
[:the
carrier of G, the
carrier of G:]
proof
let t be
object;
assume t
in S;
then ex x,y be
Element of G st t
=
[x, y] & (y
* (x
" ))
in U;
hence thesis;
end;
hence thesis;
end;
end
definition
let TG be non
empty
TopologicalGroup;
::
UNIFORM3:def10
func
system_right_uniformity (TG) -> non
empty
Subset-Family of
[:the
carrier of TG, the
carrier of TG:] equals the set of all (
element_right_uniformity U) where U be
a_neighborhood of (
1_ TG);
coherence
proof
set SF = the set of all (
element_right_uniformity U) where U be
a_neighborhood of (
1_ TG);
reconsider nG = (
[#] TG) as
a_neighborhood of (
1_ TG) by
TOPGRP_1: 21;
A1: (
element_right_uniformity nG)
in SF;
SF
c= (
bool
[:the
carrier of TG, the
carrier of TG:])
proof
let t be
object;
assume t
in SF;
then ex U be
a_neighborhood of (
1_ TG) st t
= (
element_right_uniformity U);
hence thesis;
end;
hence thesis by
A1;
end;
end
definition
let TG be non
empty
TopologicalGroup;
::
UNIFORM3:def11
func
right_uniformity (TG) -> non
empty
UniformSpace equals
UniformSpaceStr (# the
carrier of TG,
<.(
system_right_uniformity TG).] #);
coherence
proof
set cB = (
system_right_uniformity TG);
now
now
let B1,B2 be
Element of cB;
B1
in (
system_right_uniformity TG);
then
consider U1 be
a_neighborhood of (
1_ TG) such that
A1: B1
= (
element_right_uniformity U1);
B2
in (
system_right_uniformity TG);
then
consider U2 be
a_neighborhood of (
1_ TG) such that
A2: B2
= (
element_right_uniformity U2);
reconsider U3 = (U1
/\ U2) as
a_neighborhood of (
1_ TG) by
CONNSP_2: 2;
set B3 = (
element_right_uniformity U3);
B3
in cB;
then
reconsider B3 as
Element of cB;
B3
c= (B1
/\ B2)
proof
let t be
object;
assume t
in B3;
then
consider x,y be
Element of TG such that
A3: t
=
[x, y] and
A4: (y
* (x
" ))
in U3;
(y
* (x
" ))
in U1 & (y
* (x
" ))
in U2 by
A4,
XBOOLE_0:def 4;
then t
in B1 & t
in B2 by
A3,
A1,
A2;
hence thesis by
XBOOLE_0:def 4;
end;
hence ex B3 be
Element of cB st B3
c= (B1
/\ B2);
end;
hence cB is
quasi_basis;
now
let B be
Element of cB;
B
in (
system_right_uniformity TG);
then
consider U be
a_neighborhood of (
1_ TG) such that
A5: B
= (
element_right_uniformity U);
now
let t be
object;
assume
A6: t
in (
id the
carrier of TG);
then
consider x,y be
object such that
A7: x
in the
carrier of TG and
A8: y
in the
carrier of TG and
A9: t
=
[x, y] by
ZFMISC_1:def 2;
reconsider x, y as
Element of TG by
A7,
A8;
x
= y by
A6,
A9,
RELAT_1:def 10;
then (y
* (x
" ))
= (
1_ TG) by
GROUP_1:def 5;
then x is
Element of TG & y is
Element of TG & (y
* (x
" ))
in U by
CONNSP_2: 4;
hence t
in B by
A5,
A9;
end;
hence (
id the
carrier of TG)
c= B;
end;
hence cB is
axiom_UP1;
now
let B1 be
Element of cB;
B1
in (
system_right_uniformity TG);
then
consider U be
a_neighborhood of (
1_ TG) such that
A10: B1
= (
element_right_uniformity U);
consider R1 be
Relation of the
carrier of TG such that
A11: B1
= R1 and
A12: (R1
~ )
= (B1
~ );
(U
" ) is
a_neighborhood of ((
1_ TG)
" ) by
TOPGRP_1: 54;
then
reconsider U2 = (U
" ) as
a_neighborhood of (
1_ TG) by
GROUP_1: 8;
set B2 = (
element_right_uniformity U2);
B2
in cB;
then
reconsider B2 as
Element of cB;
B2
c= (B1
~ )
proof
let t be
object;
assume t
in B2;
then
consider a,b be
Element of TG such that
A13: t
=
[a, b] and
A14: (b
* (a
" ))
in U2;
consider g be
Element of TG such that
A15: (b
* (a
" ))
= (g
" ) and
A16: g
in U by
A14;
((b
* (a
" ))
" )
in U by
A15,
A16;
then (((a
" )
" )
* (b
" ))
in U by
GROUP_1: 17;
then
[b, a]
in R1 by
A10,
A11;
hence thesis by
A12,
A13,
RELAT_1:def 7;
end;
hence ex B2 be
Element of cB st B2
c= (B1
~ );
end;
hence cB is
axiom_UP2;
now
let B1 be
Element of cB;
B1
in (
system_right_uniformity TG);
then
consider U be
a_neighborhood of (
1_ TG) such that
A17: B1
= (
element_right_uniformity U);
U is
a_neighborhood of ((
1_ TG)
* (
1_ TG)) by
GROUP_1:def 4;
then
consider A be
open
a_neighborhood of (
1_ TG), B be
open
a_neighborhood of (
1_ TG) such that
A17bis: (A
* B)
c= U by
TOPGRP_1: 37;
reconsider AB = (A
/\ B) as
a_neighborhood of (
1_ TG) by
CONNSP_2: 2;
AB
c= A & AB
c= B by
XBOOLE_1: 17;
then
A18: (AB
* AB)
c= (A
* B) by
GROUP_3: 4;
set B2 = (
element_right_uniformity AB);
B2
in cB;
then
reconsider B2 as
Element of cB;
(B2
* B2)
c= B1
proof
let t be
object;
assume
A19: t
in (B2
* B2);
consider R1,R2 be
Relation of the
carrier of TG such that
A20: R1
= B2 and R2
= B2 and (B2
* B2)
= (R1
* R2);
t
in {
[x, y] where x,y be
Element of TG : ex z be
Element of TG st
[x, z]
in R1 &
[z, y]
in R1 } by
A19,
A20,
UNIFORM2: 3;
then
consider x,y be
Element of TG such that
A23: t
=
[x, y] and
A24: ex z be
Element of TG st
[x, z]
in R1 &
[z, y]
in R1;
consider z be
Element of TG such that
A25:
[x, z]
in R1 and
A26:
[z, y]
in R1 by
A24;
consider a,b be
Element of TG such that
A27:
[x, z]
=
[a, b] and
A28: (b
* (a
" ))
in AB by
A20,
A25;
A29: x
= a & z
= b by
A27,
XTUPLE_0: 1;
consider c,d be
Element of TG such that
A30:
[z, y]
=
[c, d] and
A31: (d
* (c
" ))
in AB by
A26,
A20;
A32: z
= c & y
= d by
A30,
XTUPLE_0: 1;
A33: ((d
* (c
" ))
* (b
* (a
" )))
= (y
* ((z
" )
* (z
* (x
" )))) by
A29,
A32,
GROUP_1:def 3
.= (y
* (((z
" )
* z)
* (x
" ))) by
GROUP_1:def 3
.= (y
* ((
1_ TG)
* (x
" ))) by
GROUP_1:def 5
.= (y
* (x
" )) by
GROUP_1:def 4;
((d
* (c
" ))
* (b
* (a
" )))
in (AB
* AB) by
A31,
A28;
then (y
* (x
" ))
in U by
A18,
A33,
A17bis;
hence t
in B1 by
A17,
A23;
end;
hence ex B2 be
Element of cB st (B2
* B2)
c= B1;
end;
hence cB is
axiom_UP3;
end;
then ex US be
strict
UniformSpace st the
carrier of US
= the
carrier of TG & the
entourages of US
=
<.cB.] by
Th7;
hence thesis;
end;
end
theorem ::
UNIFORM3:24
Th12: for TG be non
empty
commutative
TopologicalGroup, U be
a_neighborhood of (
1_ TG) holds (
element_left_uniformity U)
= (
element_right_uniformity U)
proof
let TG be non
empty
commutative
TopologicalGroup, U be
a_neighborhood of (
1_ TG);
now
thus (
element_left_uniformity U)
c= (
element_right_uniformity U)
proof
let x be
object;
assume x
in (
element_left_uniformity U);
then
consider u,v be
Element of TG such that
A1: x
=
[u, v] and
A2: ((u
" )
* v)
in U;
(v
* (u
" ))
in U by
A2,
GROUP_1:def 12;
hence thesis by
A1;
end;
thus (
element_right_uniformity U)
c= (
element_left_uniformity U)
proof
let x be
object;
assume x
in (
element_right_uniformity U);
then
consider u,v be
Element of TG such that
A3: x
=
[u, v] and
A4: (v
* (u
" ))
in U;
((u
" )
* v)
in U by
A4,
GROUP_1:def 12;
hence thesis by
A3;
end;
end;
hence thesis;
end;
theorem ::
UNIFORM3:25
for TG be non
empty
commutative
TopologicalGroup holds (
left_uniformity TG)
= (
right_uniformity TG)
proof
let TG be non
empty
commutative
TopologicalGroup;
set X = the set of all (
element_left_uniformity U) where U be
a_neighborhood of (
1_ TG);
set Y = the set of all (
element_right_uniformity U) where U be
a_neighborhood of (
1_ TG);
now
thus X
c= Y
proof
let x be
object;
assume x
in X;
then
consider U be
a_neighborhood of (
1_ TG) such that
A1: x
= (
element_left_uniformity U);
x
= (
element_right_uniformity U) by
A1,
Th12;
hence thesis;
end;
thus Y
c= X
proof
let x be
object;
assume x
in Y;
then
consider U be
a_neighborhood of (
1_ TG) such that
A2: x
= (
element_right_uniformity U);
x
= (
element_left_uniformity U) by
A2,
Th12;
hence thesis;
end;
end;
then (
system_left_uniformity TG)
= (
system_right_uniformity TG);
hence thesis;
end;
definition
let G be
TopaddGroup;
let U be
a_neighborhood of (
0_ G);
::
UNIFORM3:def12
func
element_left_uniformity (U) ->
Subset of
[:the
carrier of G, the
carrier of G:] equals {
[x, y] where x be
Element of G, y be
Element of G : ((
- x)
+ y)
in U };
coherence
proof
set S = {
[x, y] where x be
Element of G, y be
Element of G : ((
- x)
+ y)
in U };
S
c=
[:the
carrier of G, the
carrier of G:]
proof
let t be
object;
assume t
in S;
then ex x,y be
Element of G st t
=
[x, y] & ((
- x)
+ y)
in U;
hence thesis;
end;
hence thesis;
end;
end
definition
let TG be non
empty
TopaddGroup;
::
UNIFORM3:def13
func
system_left_uniformity (TG) -> non
empty
Subset-Family of
[:the
carrier of TG, the
carrier of TG:] equals the set of all (
element_left_uniformity U) where U be
a_neighborhood of (
0_ TG);
coherence
proof
set SF = the set of all (
element_left_uniformity U) where U be
a_neighborhood of (
0_ TG);
reconsider nG = (
[#] TG) as
a_neighborhood of (
0_ TG) by
TOPGRP_1: 21;
A1: (
element_left_uniformity nG)
in SF;
SF
c= (
bool
[:the
carrier of TG, the
carrier of TG:])
proof
let t be
object;
assume t
in SF;
then ex U be
a_neighborhood of (
0_ TG) st t
= (
element_left_uniformity U);
hence thesis;
end;
hence thesis by
A1;
end;
end
definition
let TG be non
empty
TopologicaladdGroup;
::
UNIFORM3:def14
func
left_uniformity (TG) -> non
empty
UniformSpace equals
UniformSpaceStr (# the
carrier of TG,
<.(
system_left_uniformity TG).] #);
coherence
proof
set cB = (
system_left_uniformity TG);
now
now
let B1,B2 be
Element of cB;
B1
in (
system_left_uniformity TG);
then
consider U1 be
a_neighborhood of (
0_ TG) such that
A1: B1
= (
element_left_uniformity U1);
B2
in (
system_left_uniformity TG);
then
consider U2 be
a_neighborhood of (
0_ TG) such that
A2: B2
= (
element_left_uniformity U2);
reconsider U3 = (U1
/\ U2) as
a_neighborhood of (
0_ TG) by
CONNSP_2: 2;
set B3 = (
element_left_uniformity U3);
B3
in cB;
then
reconsider B3 as
Element of cB;
B3
c= (B1
/\ B2)
proof
let t be
object;
assume t
in B3;
then
consider x,y be
Element of TG such that
A3: t
=
[x, y] and
A4: ((
- x)
+ y)
in U3;
((
- x)
+ y)
in U1 & ((
- x)
+ y)
in U2 by
A4,
XBOOLE_0:def 4;
then t
in B1 & t
in B2 by
A3,
A1,
A2;
hence thesis by
XBOOLE_0:def 4;
end;
hence ex B3 be
Element of cB st B3
c= (B1
/\ B2);
end;
hence cB is
quasi_basis;
now
let B be
Element of cB;
B
in (
system_left_uniformity TG);
then
consider U be
a_neighborhood of (
0_ TG) such that
A5: B
= (
element_left_uniformity U);
now
let t be
object;
assume
A6: t
in (
id the
carrier of TG);
then
consider x,y be
object such that
A7: x
in the
carrier of TG and
A8: y
in the
carrier of TG and
A9: t
=
[x, y] by
ZFMISC_1:def 2;
reconsider x, y as
Element of TG by
A7,
A8;
x
= y by
A6,
A9,
RELAT_1:def 10;
then ((
- x)
+ y)
= (
0_ TG) by
GROUP_1A:def 4;
then x is
Element of TG & y is
Element of TG & ((
- x)
+ y)
in U by
CONNSP_2: 4;
hence t
in B by
A5,
A9;
end;
hence (
id the
carrier of TG)
c= B;
end;
hence cB is
axiom_UP1;
now
let B1 be
Element of cB;
B1
in (
system_left_uniformity TG);
then
consider U be
a_neighborhood of (
0_ TG) such that
A10: B1
= (
element_left_uniformity U);
consider R1 be
Relation of the
carrier of TG such that
A11: B1
= R1 and
A12: (R1
~ )
= (B1
~ );
(
- U) is
a_neighborhood of (
- (
0_ TG)) by
GROUP_1A: 371;
then
reconsider U2 = (
- U) as
a_neighborhood of (
0_ TG) by
GROUP_1A: 8;
set B2 = (
element_left_uniformity U2);
B2
in cB;
then
reconsider B2 as
Element of cB;
B2
c= (B1
~ )
proof
let t be
object;
assume t
in B2;
then
consider a,b be
Element of TG such that
A13: t
=
[a, b] and
A14: ((
- a)
+ b)
in U2;
consider g be
Element of TG such that
A15: ((
- a)
+ b)
= (
- g) and
A16: g
in U by
A14;
(
- ((
- a)
+ b))
in U by
A15,
A16;
then ((
- b)
+ (
- (
- a)))
in U by
GROUP_1A: 16;
then
[b, a]
in R1 by
A10,
A11;
hence thesis by
A12,
A13,
RELAT_1:def 7;
end;
hence ex B2 be
Element of cB st B2
c= (B1
~ );
end;
hence cB is
axiom_UP2;
now
let B1 be
Element of cB;
B1
in (
system_left_uniformity TG);
then
consider U be
a_neighborhood of (
0_ TG) such that
A17: B1
= (
element_left_uniformity U);
U is
a_neighborhood of ((
0_ TG)
+ (
0_ TG)) by
GROUP_1A:def 3;
then
consider A be
open
a_neighborhood of (
0_ TG), B be
open
a_neighborhood of (
0_ TG) such that
A17bis: (A
+ B)
c= U by
GROUP_1A: 354;
reconsider AB = (A
/\ B) as
a_neighborhood of (
0_ TG) by
CONNSP_2: 2;
AB
c= A & AB
c= B by
XBOOLE_1: 17;
then
A18: (AB
+ AB)
c= (A
+ B) by
Th3;
set B2 = (
element_left_uniformity AB);
B2
in cB;
then
reconsider B2 as
Element of cB;
(B2
* B2)
c= B1
proof
let t be
object;
assume
A19: t
in (B2
* B2);
consider R1,R2 be
Relation of the
carrier of TG such that
A20: R1
= B2 and R2
= B2 and (B2
* B2)
= (R1
* R2);
t
in {
[x, y] where x,y be
Element of TG : ex z be
Element of TG st
[x, z]
in R1 &
[z, y]
in R1 } by
A19,
A20,
UNIFORM2: 3;
then
consider x,y be
Element of TG such that
A23: t
=
[x, y] and
A24: ex z be
Element of TG st
[x, z]
in R1 &
[z, y]
in R1;
consider z be
Element of TG such that
A25:
[x, z]
in R1 and
A26:
[z, y]
in R1 by
A24;
consider a,b be
Element of TG such that
A27:
[x, z]
=
[a, b] and
A28: ((
- a)
+ b)
in AB by
A20,
A25;
A29: x
= a & z
= b by
A27,
XTUPLE_0: 1;
consider c,d be
Element of TG such that
A30:
[z, y]
=
[c, d] and
A31: ((
- c)
+ d)
in AB by
A26,
A20;
A32: z
= c & y
= d by
A30,
XTUPLE_0: 1;
A33: (((
- a)
+ b)
+ ((
- c)
+ d))
= ((
- x)
+ (z
+ ((
- z)
+ y))) by
A29,
A32,
RLVECT_1:def 3
.= ((
- x)
+ ((z
+ (
- z))
+ y)) by
RLVECT_1:def 3
.= ((
- x)
+ ((
0_ TG)
+ y)) by
GROUP_1A:def 4
.= ((
- x)
+ y) by
GROUP_1A:def 3;
(((
- a)
+ b)
+ ((
- c)
+ d))
in (AB
+ AB) by
A28,
A31;
then ((
- x)
+ y)
in U by
A18,
A33,
A17bis;
hence t
in B1 by
A17,
A23;
end;
hence ex B2 be
Element of cB st (B2
* B2)
c= B1;
end;
hence cB is
axiom_UP3;
end;
then ex US be
strict
UniformSpace st the
carrier of US
= the
carrier of TG & the
entourages of US
=
<.cB.] by
Th7;
hence thesis;
end;
end
definition
let G be
TopaddGroup;
let U be
a_neighborhood of (
0_ G);
::
UNIFORM3:def15
func
element_right_uniformity (U) ->
Subset of
[:the
carrier of G, the
carrier of G:] equals {
[x, y] where x be
Element of G, y be
Element of G : (y
+ (
- x))
in U };
coherence
proof
set S = {
[x, y] where x be
Element of G, y be
Element of G : (y
+ (
- x))
in U };
S
c=
[:the
carrier of G, the
carrier of G:]
proof
let t be
object;
assume t
in S;
then ex x,y be
Element of G st t
=
[x, y] & (y
+ (
- x))
in U;
hence thesis;
end;
hence thesis;
end;
end
definition
let TG be non
empty
TopaddGroup;
::
UNIFORM3:def16
func
system_right_uniformity (TG) -> non
empty
Subset-Family of
[:the
carrier of TG, the
carrier of TG:] equals the set of all (
element_right_uniformity U) where U be
a_neighborhood of (
0_ TG);
coherence
proof
set SF = the set of all (
element_right_uniformity U) where U be
a_neighborhood of (
0_ TG);
reconsider nG = (
[#] TG) as
a_neighborhood of (
0_ TG) by
TOPGRP_1: 21;
A1: (
element_right_uniformity nG)
in SF;
SF
c= (
bool
[:the
carrier of TG, the
carrier of TG:])
proof
let t be
object;
assume t
in SF;
then ex U be
a_neighborhood of (
0_ TG) st t
= (
element_right_uniformity U);
hence thesis;
end;
hence thesis by
A1;
end;
end
definition
let TG be non
empty
TopologicaladdGroup;
::
UNIFORM3:def17
func
right_uniformity (TG) -> non
empty
UniformSpace equals
UniformSpaceStr (# the
carrier of TG,
<.(
system_right_uniformity TG).] #);
coherence
proof
set cB = (
system_right_uniformity TG);
now
now
let B1,B2 be
Element of cB;
B1
in (
system_right_uniformity TG);
then
consider U1 be
a_neighborhood of (
0_ TG) such that
A1: B1
= (
element_right_uniformity U1);
B2
in (
system_right_uniformity TG);
then
consider U2 be
a_neighborhood of (
0_ TG) such that
A2: B2
= (
element_right_uniformity U2);
reconsider U3 = (U1
/\ U2) as
a_neighborhood of (
0_ TG) by
CONNSP_2: 2;
set B3 = (
element_right_uniformity U3);
B3
in cB;
then
reconsider B3 as
Element of cB;
B3
c= (B1
/\ B2)
proof
let t be
object;
assume t
in B3;
then
consider x,y be
Element of TG such that
A3: t
=
[x, y] and
A4: (y
+ (
- x))
in U3;
(y
+ (
- x))
in U1 & (y
+ (
- x))
in U2 by
A4,
XBOOLE_0:def 4;
then t
in B1 & t
in B2 by
A3,
A1,
A2;
hence thesis by
XBOOLE_0:def 4;
end;
hence ex B3 be
Element of cB st B3
c= (B1
/\ B2);
end;
hence cB is
quasi_basis;
now
let B be
Element of cB;
B
in (
system_right_uniformity TG);
then
consider U be
a_neighborhood of (
0_ TG) such that
A5: B
= (
element_right_uniformity U);
now
let t be
object;
assume
A6: t
in (
id the
carrier of TG);
then
consider x,y be
object such that
A7: x
in the
carrier of TG and
A8: y
in the
carrier of TG and
A9: t
=
[x, y] by
ZFMISC_1:def 2;
reconsider x, y as
Element of TG by
A7,
A8;
x
= y by
A6,
A9,
RELAT_1:def 10;
then (y
+ (
- x))
= (
0_ TG) by
GROUP_1A:def 4;
then x is
Element of TG & y is
Element of TG & (y
+ (
- x))
in U by
CONNSP_2: 4;
hence t
in B by
A5,
A9;
end;
hence (
id the
carrier of TG)
c= B;
end;
hence cB is
axiom_UP1;
now
let B1 be
Element of cB;
B1
in (
system_right_uniformity TG);
then
consider U be
a_neighborhood of (
0_ TG) such that
A10: B1
= (
element_right_uniformity U);
consider R1 be
Relation of the
carrier of TG such that
A11: B1
= R1 and
A12: (R1
~ )
= (B1
~ );
(
- U) is
a_neighborhood of (
- (
0_ TG)) by
GROUP_1A: 371;
then
reconsider U2 = (
- U) as
a_neighborhood of (
0_ TG) by
GROUP_1A: 8;
set B2 = (
element_right_uniformity U2);
B2
in cB;
then
reconsider B2 as
Element of cB;
B2
c= (B1
~ )
proof
let t be
object;
assume t
in B2;
then
consider a,b be
Element of TG such that
A13: t
=
[a, b] and
A14: (b
+ (
- a))
in U2;
consider g be
Element of TG such that
A15: (b
+ (
- a))
= (
- g) and
A16: g
in U by
A14;
(
- (b
+ (
- a)))
in U by
A15,
A16;
then ((
- (
- a))
+ (
- b))
in U by
GROUP_1A: 16;
then
[b, a]
in R1 by
A10,
A11;
hence thesis by
A12,
A13,
RELAT_1:def 7;
end;
hence ex B2 be
Element of cB st B2
c= (B1
~ );
end;
hence cB is
axiom_UP2;
now
let B1 be
Element of cB;
B1
in (
system_right_uniformity TG);
then
consider U be
a_neighborhood of (
0_ TG) such that
A17: B1
= (
element_right_uniformity U);
U is
a_neighborhood of ((
0_ TG)
+ (
0_ TG)) by
GROUP_1A:def 3;
then
consider A be
open
a_neighborhood of (
0_ TG), B be
open
a_neighborhood of (
0_ TG) such that
A17bis: (A
+ B)
c= U by
GROUP_1A: 354;
reconsider AB = (A
/\ B) as
a_neighborhood of (
0_ TG) by
CONNSP_2: 2;
AB
c= A & AB
c= B by
XBOOLE_1: 17;
then
A18: (AB
+ AB)
c= (A
+ B) by
Th3;
set B2 = (
element_right_uniformity AB);
B2
in cB;
then
reconsider B2 as
Element of cB;
(B2
* B2)
c= B1
proof
let t be
object;
assume
A19: t
in (B2
* B2);
consider R1,R2 be
Relation of the
carrier of TG such that
A20: R1
= B2 and R2
= B2 and (B2
* B2)
= (R1
* R2);
t
in {
[x, y] where x,y be
Element of TG : ex z be
Element of TG st
[x, z]
in R1 &
[z, y]
in R1 } by
A19,
A20,
UNIFORM2: 3;
then
consider x,y be
Element of TG such that
A23: t
=
[x, y] and
A24: ex z be
Element of TG st
[x, z]
in R1 &
[z, y]
in R1;
consider z be
Element of TG such that
A25:
[x, z]
in R1 and
A26:
[z, y]
in R1 by
A24;
consider a,b be
Element of TG such that
A27:
[x, z]
=
[a, b] and
A28: (b
+ (
- a))
in AB by
A20,
A25;
A29: x
= a & z
= b by
A27,
XTUPLE_0: 1;
consider c,d be
Element of TG such that
A30:
[z, y]
=
[c, d] and
A31: (d
+ (
- c))
in AB by
A26,
A20;
A32: z
= c & y
= d by
A30,
XTUPLE_0: 1;
A33: ((d
+ (
- c))
+ (b
+ (
- a)))
= (y
+ ((
- z)
+ (z
+ (
- x)))) by
A29,
A32,
RLVECT_1:def 3
.= (y
+ (((
- z)
+ z)
+ (
- x))) by
RLVECT_1:def 3
.= (y
+ ((
0_ TG)
+ (
- x))) by
GROUP_1A:def 4
.= (y
+ (
- x)) by
GROUP_1A:def 3;
((d
+ (
- c))
+ (b
+ (
- a)))
in (AB
+ AB) by
A28,
A31;
then (y
+ (
- x))
in U by
A18,
A33,
A17bis;
hence t
in B1 by
A17,
A23;
end;
hence ex B2 be
Element of cB st (B2
* B2)
c= B1;
end;
hence cB is
axiom_UP3;
end;
then ex US be
strict
UniformSpace st the
carrier of US
= the
carrier of TG & the
entourages of US
=
<.cB.] by
Th7;
hence thesis;
end;
end
theorem ::
UNIFORM3:26
Th13: for TG be
Abelian
TopaddGroup, U be
a_neighborhood of (
0_ TG) holds (
element_left_uniformity U)
= (
element_right_uniformity U)
proof
let TG be
Abelian
TopaddGroup, U be
a_neighborhood of (
0_ TG);
now
thus (
element_left_uniformity U)
c= (
element_right_uniformity U)
proof
let x be
object;
assume x
in (
element_left_uniformity U);
then ex u,v be
Element of TG st x
=
[u, v] & ((
- u)
+ v)
in U;
hence thesis;
end;
thus (
element_right_uniformity U)
c= (
element_left_uniformity U)
proof
let x be
object;
assume x
in (
element_right_uniformity U);
then ex u,v be
Element of TG st x
=
[u, v] & (v
+ (
- u))
in U;
hence thesis;
end;
end;
hence thesis;
end;
theorem ::
UNIFORM3:27
for TG be non
empty
TopologicaladdGroup st TG is
Abelian holds (
left_uniformity TG)
= (
right_uniformity TG)
proof
let TG be non
empty
TopologicaladdGroup;
assume
A1: TG is
Abelian;
set X = the set of all (
element_left_uniformity U) where U be
a_neighborhood of (
0_ TG);
set Y = the set of all (
element_right_uniformity U) where U be
a_neighborhood of (
0_ TG);
now
thus X
c= Y
proof
let x be
object;
assume x
in X;
then
consider U be
a_neighborhood of (
0_ TG) such that
A2: x
= (
element_left_uniformity U);
x
= (
element_right_uniformity U) by
A1,
A2,
Th13;
hence thesis;
end;
thus Y
c= X
proof
let x be
object;
assume x
in Y;
then
consider U be
a_neighborhood of (
0_ TG) such that
A3: x
= (
element_right_uniformity U);
x
= (
element_left_uniformity U) by
A1,
A3,
Th13;
hence thesis;
end;
end;
then (
system_left_uniformity TG)
= (
system_right_uniformity TG);
hence thesis;
end;
theorem ::
UNIFORM3:28
the
topology of (
TopSpace_induced_by (
left_uniformity TG))
= the
topology of TG
proof
set X = the
topology of (
FMT2TopSpace (
FMT_induced_by (
left_uniformity TG))), Y = the
topology of TG;
A2: X
c= Y
proof
let x be
object;
assume x
in X;
then x
in (
Family_open_set (
FMT_induced_by (
left_uniformity TG))) by
FINTOPO7:def 16;
then
consider y be
open
Subset of (
FMT_induced_by (
left_uniformity TG)) such that
A3: x
= y;
reconsider z = x as
Subset of TG by
A3;
z is
open
proof
now
let t be
Point of TG;
assume
A4: t
in z;
reconsider t1 = t as
Point of (
FMT_induced_by (
left_uniformity TG));
A5: y
in (
U_FMT t1) by
A3,
A4,
FINTOPO7:def 1;
reconsider t2 = t1 as
Element of (
left_uniformity TG);
z
in (
Neighborhood t2) by
A3,
A5,
UNIFORM2:def 14;
then
consider V0 be
Element of the
entourages of (
left_uniformity TG) such that
A6: z
= (
Neighborhood (V0,t2));
consider tg be
Element of (
system_left_uniformity TG) such that
A7: tg
c= V0 by
CARDFIL2:def 8;
tg
in the set of all (
element_left_uniformity U) where U be
a_neighborhood of (
1_ TG);
then
consider U0 be
a_neighborhood of (
1_ TG) such that
A8: tg
= (
element_left_uniformity U0);
reconsider A = (
{t}
* U0) as
a_neighborhood of t by
Th4;
A
c= z
proof
let u be
object;
assume u
in A;
then
consider u0,u1 be
Element of TG such that
A9: u
= (u0
* u1) and
A10: u0
in
{t} and
A11: u1
in U0;
reconsider u2 = u as
Element of TG by
A9;
((
1_ TG)
* u1)
in U0 by
A11,
GROUP_1:def 4;
then (((t
" )
* t)
* u1)
in U0 by
GROUP_1:def 5;
then ((t
" )
* (t
* u1))
in U0 by
GROUP_1:def 3;
then ((t
" )
* u2)
in U0 by
A9,
A10,
TARSKI:def 1;
then
[t, u2]
in (
element_left_uniformity U0);
hence thesis by
A6,
A7,
A8;
end;
hence ex A be
Subset of TG st A is
a_neighborhood of t & A
c= z;
end;
hence thesis by
CONNSP_2: 7;
end;
hence x
in Y;
end;
Y
c= X
proof
let u be
object;
assume
A12: u
in Y;
then
reconsider u as
Subset of TG;
reconsider v = u as
Subset of (
FMT_induced_by (
left_uniformity TG));
for x be
Element of (
FMT_induced_by (
left_uniformity TG)) st x
in v holds v
in (
U_FMT x)
proof
let x be
Element of (
FMT_induced_by (
left_uniformity TG));
assume
A13: x
in v;
reconsider t2 = x as
Element of (
left_uniformity TG);
reconsider t3 = x as
Element of TG;
reconsider w = v as
Subset of TG;
now
{(t3
" )}
= (
{t3}
" ) by
GROUP_2: 3;
then (t3
" )
in (
{t3}
" ) by
TARSKI:def 1;
then ((t3
" )
* t3)
in ((
{t3}
" )
* w) by
A13;
hence (
1_ TG)
in ((
{t3}
" )
* w) by
GROUP_1:def 5;
w is
open by
A12;
hence ((
{t3}
" )
* w) is
open;
end;
then
reconsider U0 = ((
{t3}
" )
* w) as
a_neighborhood of (
1_ TG) by
CONNSP_2: 6;
(
element_left_uniformity U0)
in (
system_left_uniformity TG);
then
reconsider V0 = (
element_left_uniformity U0) as
Element of the
entourages of (
left_uniformity TG) by
CARDFIL2:def 8;
v
= { y where y be
Element of TG :
[t2, y]
in V0 }
proof
set v2 = { y where y be
Element of TG :
[t2, y]
in V0 };
A15: v
c= v2
proof
let t be
object;
assume
A16: t
in v;
then
reconsider t4 = t as
Element of TG;
{(t3
" )}
= (
{t3}
" ) by
GROUP_2: 3;
then
A17: (t3
" )
in (
{t3}
" ) by
TARSKI:def 1;
((t3
" )
* t4)
in ((
{t3}
" )
* w) by
A16,
A17;
then
[t2, t4]
in (
element_left_uniformity U0);
hence thesis;
end;
v2
c= v
proof
let t be
object;
assume t
in v2;
then
consider y0 be
Element of TG such that
A18: t
= y0 and
A19:
[t2, y0]
in V0;
consider xt,yt be
Element of TG such that
A20:
[t2, y0]
=
[xt, yt] and
A21: ((xt
" )
* yt)
in U0 by
A19;
t2
= xt & y0
= yt by
A20,
XTUPLE_0: 1;
then
consider u1,u2 be
Element of TG such that
A22: ((t3
" )
* y0)
= (u1
* u2) and
A23: u1
in (
{t3}
" ) and
A24: u2
in w by
A21;
{(t3
" )}
= (
{t3}
" ) by
GROUP_2: 3;
then u1
= (t3
" ) by
A23,
TARSKI:def 1;
hence thesis by
A18,
A22,
A24,
GROUP_1: 6;
end;
hence thesis by
A15;
end;
then v
= (
Neighborhood (V0,t2));
then v
in (
Neighborhood t2);
hence thesis by
UNIFORM2:def 14;
end;
then v is
open;
then u
in (
Family_open_set (
FMT_induced_by (
left_uniformity TG)));
hence thesis by
FINTOPO7:def 16;
end;
hence thesis by
A2;
end;
theorem ::
UNIFORM3:29
the
topology of (
TopSpace_induced_by (
right_uniformity TG))
= the
topology of TG
proof
set X = the
topology of (
FMT2TopSpace (
FMT_induced_by (
right_uniformity TG))), Y = the
topology of TG;
A2: X
c= Y
proof
let x be
object;
assume x
in X;
then x
in (
Family_open_set (
FMT_induced_by (
right_uniformity TG))) by
FINTOPO7:def 16;
then
consider y be
open
Subset of (
FMT_induced_by (
right_uniformity TG)) such that
A3: x
= y;
reconsider z = x as
Subset of TG by
A3;
z is
open
proof
now
let t be
Point of TG;
assume
A4: t
in z;
reconsider t1 = t as
Point of (
FMT_induced_by (
right_uniformity TG));
A5: y
in (
U_FMT t1) by
A3,
A4,
FINTOPO7:def 1;
reconsider t2 = t1 as
Element of (
right_uniformity TG);
z
in (
Neighborhood t2) by
A3,
A5,
UNIFORM2:def 14;
then
consider V0 be
Element of the
entourages of (
right_uniformity TG) such that
A6: z
= (
Neighborhood (V0,t2));
consider tg be
Element of (
system_right_uniformity TG) such that
A7: tg
c= V0 by
CARDFIL2:def 8;
tg
in the set of all (
element_right_uniformity U) where U be
a_neighborhood of (
1_ TG);
then
consider U0 be
a_neighborhood of (
1_ TG) such that
A8: tg
= (
element_right_uniformity U0);
reconsider A = (U0
*
{t}) as
a_neighborhood of t by
Th5;
A
c= z
proof
let u be
object;
assume u
in A;
then
consider u0,u1 be
Element of TG such that
A9: u
= (u0
* u1) and
A10: u0
in U0 and
A11: u1
in
{t};
reconsider u2 = u as
Element of TG by
A9;
(u0
* (
1_ TG))
in U0 by
A10,
GROUP_1:def 4;
then (u0
* (t
* (t
" )))
in U0 by
GROUP_1:def 5;
then ((u0
* t)
* (t
" ))
in U0 by
GROUP_1:def 3;
then (u2
* (t
" ))
in U0 by
A9,
A11,
TARSKI:def 1;
then
[t, u2]
in (
element_right_uniformity U0);
hence thesis by
A6,
A7,
A8;
end;
hence ex A be
Subset of TG st A is
a_neighborhood of t & A
c= z;
end;
hence thesis by
CONNSP_2: 7;
end;
hence x
in Y;
end;
Y
c= X
proof
let u be
object;
assume
A12: u
in Y;
then
reconsider u as
Subset of TG;
reconsider v = u as
Subset of (
FMT_induced_by (
right_uniformity TG));
for x be
Element of (
FMT_induced_by (
right_uniformity TG)) st x
in v holds v
in (
U_FMT x)
proof
let x be
Element of (
FMT_induced_by (
right_uniformity TG));
assume
A13: x
in v;
reconsider t2 = x as
Element of (
right_uniformity TG);
reconsider t3 = x as
Element of TG;
reconsider w = v as
Subset of TG;
now
{(t3
" )}
= (
{t3}
" ) by
GROUP_2: 3;
then (t3
" )
in (
{t3}
" ) by
TARSKI:def 1;
then (t3
* (t3
" ))
in (w
* (
{t3}
" )) by
A13;
hence (
1_ TG)
in (w
* (
{t3}
" )) by
GROUP_1:def 5;
w is
open by
A12;
hence (w
* (
{t3}
" )) is
open;
end;
then
reconsider U0 = (w
* (
{t3}
" )) as
a_neighborhood of (
1_ TG) by
CONNSP_2: 6;
(
element_right_uniformity U0)
in (
system_right_uniformity TG);
then
reconsider V0 = (
element_right_uniformity U0) as
Element of the
entourages of (
right_uniformity TG) by
CARDFIL2:def 8;
v
= { y where y be
Element of TG :
[t2, y]
in V0 }
proof
set v2 = { y where y be
Element of TG :
[t2, y]
in V0 };
A15: v
c= v2
proof
let t be
object;
assume
A16: t
in v;
then
reconsider t4 = t as
Element of TG;
{(t3
" )}
= (
{t3}
" ) by
GROUP_2: 3;
then (t3
" )
in (
{t3}
" ) by
TARSKI:def 1;
then (t4
* (t3
" ))
in (w
* (
{t3}
" )) by
A16;
then
[t2, t4]
in (
element_right_uniformity U0);
hence thesis;
end;
v2
c= v
proof
let t be
object;
assume t
in v2;
then
consider y0 be
Element of TG such that
A18: t
= y0 and
A19:
[t2, y0]
in V0;
consider xt,yt be
Element of TG such that
A20:
[t2, y0]
=
[xt, yt] and
A21: (yt
* (xt
" ))
in U0 by
A19;
t2
= xt & y0
= yt by
A20,
XTUPLE_0: 1;
then
consider u1,u2 be
Element of TG such that
A22: (y0
* (t3
" ))
= (u1
* u2) and
A23: u1
in w and
A24: u2
in (
{t3}
" ) by
A21;
{(t3
" )}
= (
{t3}
" ) by
GROUP_2: 3;
then u2
= (t3
" ) by
A24,
TARSKI:def 1;
hence thesis by
A22,
A23,
A18,
GROUP_1: 6;
end;
hence thesis by
A15;
end;
then v
= (
Neighborhood (V0,t2));
then v
in (
Neighborhood t2);
hence thesis by
UNIFORM2:def 14;
end;
then v is
open;
then u
in (
Family_open_set (
FMT_induced_by (
right_uniformity TG)));
hence thesis by
FINTOPO7:def 16;
end;
hence thesis by
A2;
end;
begin
definition
let US1,US2 be
UniformSpaceStr, f be
Function of US1, US2;
::
UNIFORM3:def18
attr f is
uniformly_continuous means for V be
Element of the
entourages of US2 holds ex U be
Element of the
entourages of US1 st for x,y be
object st
[x, y]
in U holds
[(f
. x), (f
. y)]
in V;
end
registration
let US1,US2 be non
empty
axiom_U1
UniformSpaceStr;
cluster
uniformly_continuous for
Function of US1, US2;
existence
proof
set e = the
Element of US2;
set f = (US1
--> e);
for V be
Element of the
entourages of US2 holds ex U be
Element of the
entourages of US1 st for x,y be
object st
[x, y]
in U holds
[(f
. x), (f
. y)]
in V
proof
let V be
Element of the
entourages of US2;
per cases ;
suppose
A1:
[e, e]
in V;
set U = the
Element of the
entourages of US1;
take U;
thus for x,y be
object st
[x, y]
in U holds
[(f
. x), (f
. y)]
in V
proof
let x,y be
object;
assume
A2:
[x, y]
in U;
consider a,b be
object such that
A3: a
in the
carrier of US1 and
A4: b
in the
carrier of US1 and
A5:
[x, y]
=
[a, b] by
A2,
ZFMISC_1:def 2;
A6: x
= a & y
= b by
A5,
XTUPLE_0: 1;
(f
. b)
= e by
A4,
FUNCOP_1: 7;
hence thesis by
A1,
A6,
A3,
FUNCOP_1: 7;
end;
end;
suppose
A8: not
[e, e]
in V;
US2 is
axiom_U1;
then
A9: (
id the
carrier of US2)
c= V;
[e, e]
in (
id the
carrier of US2) by
RELAT_1:def 10;
hence thesis by
A8,
A9;
end;
end;
then f is
uniformly_continuous;
hence thesis;
end;
end
begin
theorem ::
UNIFORM3:30
Th14: the set of all (
union P) where P be
Subset of D
= (
UniCl D)
proof
set F = the set of all (
union P) where P be
Subset of D;
thus F
c= (
UniCl D)
proof
let x be
object;
assume x
in F;
then
consider P be
Subset of D such that
A2: x
= (
union P);
P
c= D & D
c= (
bool X);
then P
c= (
bool X);
then
reconsider Y = P as
Subset-Family of X;
Y
c= D & (
union Y)
= (
union P);
hence thesis by
A2,
CANTOR_1:def 1;
end;
let x be
object;
assume x
in (
UniCl D);
then
consider Y be
Subset-Family of X such that
A3: Y
c= D and
A4: x
= (
union Y) by
CANTOR_1:def 1;
reconsider P = Y as
Subset of D by
A3;
x
= (
union P) by
A4;
hence thesis;
end;
theorem ::
UNIFORM3:31
Th15: X
in (
UniCl D)
proof
D
c= D;
then (
union D)
in the set of all (
union P) where P be
Subset of D;
then X
in the set of all (
union P) where P be
Subset of D by
EQREL_1:def 4;
hence thesis by
Th14;
end;
theorem ::
UNIFORM3:32
Th16: D
=
{} implies X is
empty & (
UniCl D)
=
{
{} } by
ZFMISC_1: 2,
EQREL_1:def 4,
YELLOW_9: 16;
registration
let X be
set, D be
a_partition of X;
cluster (
UniCl D) ->
cap-closed;
coherence
proof
set DU = the set of all (
union P) where P be
Subset of D;
now
let a,b be
set;
assume that
A1: a
in DU and
A2: b
in DU;
consider Pa be
Subset of D such that
A3: a
= (
union Pa) by
A1;
consider Pb be
Subset of D such that
A4: b
= (
union Pb) by
A2;
now
let X,Y be
set;
assume that
A5: X
<> Y and
A6: X
in (Pa
\/ Pb) and
A7: Y
in (Pa
\/ Pb);
X
in D & Y
in D by
A6,
A7;
hence X
misses Y by
A5,
EQREL_1:def 4;
end;
then ((
union Pa)
/\ (
union Pb))
= (
union (Pa
/\ Pb)) by
ZFMISC_1: 83;
hence (a
/\ b)
in DU by
A3,
A4;
end;
then DU is
cap-closed;
hence thesis by
Th14;
end;
end
registration
let X be
set, D be
a_partition of X;
cluster (
UniCl D) ->
union-closed;
coherence
proof
the set of all (
union P) where P be
Subset of D
c= (
bool X)
proof
let x be
object;
assume x
in the set of all (
union P) where P be
Subset of D;
then
consider P be
Subset of D such that
A1: x
= (
union P);
(
union P)
c= (
union D) by
ZFMISC_1: 77;
then (
union P)
c= X by
EQREL_1:def 4;
hence thesis by
A1;
end;
then
reconsider DU = the set of all (
union P) where P be
Subset of D as
Subset-Family of X;
for a be
Subset-Family of X st a
c= DU holds (
union a)
in DU
proof
let a be
Subset-Family of X;
assume
A2: a
c= DU;
set P = { x where x be
Element of D : x
c= (
union a) };
per cases ;
suppose
A3: D
=
{} ;
then (
UniCl D)
=
{
{} } by
Th16;
then a
c=
{
{} } by
A2,
Th14;
then a
=
{} or a
=
{
{} } by
ZFMISC_1: 33;
hence (
union a)
in DU by
A3,
ZFMISC_1: 2;
end;
suppose
A4: D
<>
{} ;
P
c= D
proof
let t be
object;
assume t
in P;
then ex x be
Element of D st t
= x & x
c= (
union a);
hence thesis by
A4;
end;
then
reconsider P as
Subset of D;
(
union a)
= (
union P)
proof
thus (
union a)
c= (
union P)
proof
let x be
object;
assume x
in (
union a);
then
consider t be
set such that
A6: x
in t and
A7: t
in a by
TARSKI:def 4;
t
in DU by
A2,
A7;
then
consider Q be
Subset of D such that
A8: t
= (
union Q);
consider y be
set such that
A9: x
in y and
A10: y
in Q by
A6,
A8,
TARSKI:def 4;
reconsider y as
Element of D by
A10;
y
c= (
union a)
proof
let b be
object;
assume b
in y;
then b
in (
union Q) by
A10,
TARSKI:def 4;
hence thesis by
A7,
A8,
TARSKI:def 4;
end;
then y
in P;
hence thesis by
A9,
TARSKI:def 4;
end;
let t be
object;
assume t
in (
union P);
then
consider u be
set such that
A11: t
in u and
A12: u
in P by
TARSKI:def 4;
ex xu be
Element of D st u
= xu & xu
c= (
union a) by
A12;
hence thesis by
A11;
end;
hence (
union a)
in DU;
end;
end;
then DU is
union-closed;
hence thesis by
Th14;
end;
end
registration
let X be
set;
cluster
union-closed ->
cup-closed for
Subset-Family of X;
coherence
proof
now
let SF be
Subset-Family of X;
assume
A1: SF is
union-closed;
now
let a,b be
set;
assume that
A2: a
in SF and
A3: b
in SF;
A4:
{a, b}
c= SF by
A2,
A3,
TARSKI:def 2;
SF
c= (
bool X);
then
{a, b}
c= (
bool X) by
A4;
then
reconsider c =
{a, b} as
Subset-Family of X;
{a, b}
c= SF by
A2,
A3,
TARSKI:def 2;
then (
union c)
in SF by
A1;
hence (a
\/ b)
in SF by
ZFMISC_1: 75;
end;
hence SF is
cup-closed;
end;
hence thesis;
end;
end
registration
let X be
set, D be
a_partition of X;
cluster (
UniCl D) ->
compl-closed;
coherence
proof
now
let A be
Subset of X;
assume A
in (
UniCl D);
then A
in the set of all (
union P) where P be
Subset of D by
Th14;
then
consider P be
Subset of D such that
A1: A
= (
union P);
reconsider P1 = (D
\ P) as
Subset of D by
XBOOLE_1: 36;
(
union P1)
= ((
union D)
\ (
union P)) by
Th2
.= (A
` ) by
A1,
EQREL_1:def 4;
then (A
` )
in the set of all (
union P) where P be
Subset of D;
hence (A
` )
in (
UniCl D) by
Th14;
end;
hence thesis;
end;
end
registration
let X be
set, D be
a_partition of X;
cluster (
UniCl D) ->
cup-closed
diff-closed;
coherence ;
end
theorem ::
UNIFORM3:33
(
UniCl D) is
Ring_of_sets
proof
set DU = the set of all (
union P) where P be
Subset of D;
(
UniCl D) is
cap-closed
cup-closed;
then DU is
cap-closed
cup-closed by
Th14;
then for x,y be
set st x
in DU & y
in DU holds (x
/\ y)
in DU & (x
\/ y)
in DU;
then DU is
Ring_of_sets by
COHSP_1:def 7,
LATTICE7:def 8;
hence thesis by
Th14;
end;
registration
let X, D;
cluster (
UniCl D) ->
with_empty_element;
coherence
proof
{}
c= D;
then (
union
{} )
in the set of all (
union P) where P be
Subset of D;
hence thesis by
ZFMISC_1: 2,
Th14;
end;
end
registration
let X be
set, D be
a_partition of X;
cluster (
UniCl D) -> non
empty;
coherence ;
end
theorem ::
UNIFORM3:34
(
UniCl D) is
Field_Subset of X;
registration
let X be
set, D be
a_partition of X;
cluster (
UniCl D) ->
sigma-additive;
coherence
proof
per cases ;
suppose
A1: D is
empty;
now
let M be
N_Sub_set_fam of X;
assume M
c= (
UniCl D);
then M
c=
{
{} } by
A1,
YELLOW_9: 16;
per cases by
ZFMISC_1: 33;
suppose M
=
{} ;
hence (
union M)
in (
UniCl D);
end;
suppose
A2: M
=
{
{} };
{}
c= D;
then
reconsider P =
{} as
Subset of D;
(
union P)
= (
union M) by
A2,
ZFMISC_1: 2;
then (
union M)
in the set of all (
union P) where P be
Subset of D;
hence (
union M)
in (
UniCl D) by
Th14;
end;
end;
hence thesis;
end;
suppose
A3: D is non
empty;
now
let M be
N_Sub_set_fam of X;
assume
A4: M
c= (
UniCl D);
{ p where p be
Element of D : p
c= (
union M) }
c= D
proof
let t be
object;
assume t
in { p where p be
Element of D : p
c= (
union M) };
then ex p be
Element of D st t
= p & p
c= (
union M);
hence thesis by
A3;
end;
then
reconsider P = { p where p be
Element of D : p
c= (
union M) } as
Subset of D;
(
union M)
= (
union P)
proof
thus (
union M)
c= (
union P)
proof
let t be
object;
assume t
in (
union M);
then
consider y be
set such that
A6: t
in y and
A7: y
in M by
TARSKI:def 4;
y
in (
UniCl D) by
A7,
A4;
then y
in the set of all (
union Q) where Q be
Subset of D by
Th14;
then
consider Q be
Subset of D such that
A8: y
= (
union Q);
consider z be
set such that
A9: t
in z and
A10: z
in Q by
A6,
A8,
TARSKI:def 4;
reconsider z as
Element of D by
A10;
A11: z
c= y by
A8,
A10,
ZFMISC_1: 74;
y
c= (
union M) by
A7,
ZFMISC_1: 74;
then z
c= (
union M) by
A11;
then z
in P;
hence thesis by
A9,
TARSKI:def 4;
end;
let x be
object;
assume x
in (
union P);
then
consider y be
set such that
A12: x
in y and
A13: y
in P by
TARSKI:def 4;
ex p be
Element of D st y
= p & p
c= (
union M) by
A13;
hence thesis by
A12;
end;
then (
union M)
in the set of all (
union P) where P be
Subset of D;
hence (
union M)
in (
UniCl D) by
Th14;
end;
hence thesis;
end;
end;
end
registration
let X be
set, D be
a_partition of X;
cluster (
UniCl D) ->
sigma-multiplicative;
coherence ;
end
theorem ::
UNIFORM3:35
(
UniCl D) is
SigmaField of X;
registration
let X be
set, D be
a_partition of X;
cluster (
UniCl D) ->
closed_for_countable_unions
closed_for_countable_meets;
coherence by
TOPGEN_4: 17;
end
theorem ::
UNIFORM3:36
for Omega be non
empty
set, D be
a_partition of Omega holds (
UniCl D) is
Dynkin_System of Omega
proof
let Omega be non
empty
set, D be
a_partition of Omega;
now
hereby
let f be
SetSequence of Omega;
assume that
A1: (
rng f)
c= (
UniCl D) and f is
disjoint_valued;
(
UniCl D)
c= (
bool Omega);
then (
rng f)
c= (
bool Omega) by
A1;
then
reconsider a = (
rng f) as
Subset-Family of Omega;
(
union a)
in (
UniCl D) by
A1,
ROUGHS_4:def 3;
hence (
Union f)
in (
UniCl D) by
CARD_3:def 4;
end;
thus for X be
Subset of Omega st X
in (
UniCl D) holds (X
` )
in (
UniCl D) by
PROB_1:def 1;
(
UniCl D) is
with_empty_element;
hence
{}
in (
UniCl D);
end;
hence thesis by
DYNKIN:def 5;
end;
definition
let X be
set, D be
a_partition of X;
::
UNIFORM3:def19
func
partition_topology (D) ->
TopSpace equals
TopStruct (# X, (
UniCl D) #);
coherence
proof
set TS =
TopStruct (# X, (
UniCl D) #);
(the
carrier of TS
in the
topology of TS) & (for a be
Subset-Family of TS st a
c= the
topology of TS holds (
union a)
in the
topology of TS) & (for a,b be
Subset of TS st a
in the
topology of TS & b
in the
topology of TS holds (a
/\ b)
in the
topology of TS) by
Th15,
ROUGHS_4:def 3,
FINSUB_1:def 2;
hence thesis by
PRE_TOPC:def 1;
end;
end
theorem ::
UNIFORM3:37
Th18: for O be
open
Subset of (
partition_topology D) holds O is
closed
proof
let O be
open
Subset of (
partition_topology D);
(O
` )
in (
UniCl D) by
PRE_TOPC:def 2,
PROB_1:def 1;
hence thesis by
PRE_TOPC:def 2;
end;
theorem ::
UNIFORM3:38
Th19: for O be
closed
Subset of (
partition_topology D) holds O is
open
proof
let O be
closed
Subset of (
partition_topology D);
((
[#] (
partition_topology D))
\ O)
in (
UniCl D) by
PRE_TOPC:def 2,
PRE_TOPC:def 3;
then
A1: ((X
\ O)
` )
in (
UniCl D) by
PROB_1:def 1;
O
= (X
/\ O) by
XBOOLE_1: 18,
XBOOLE_1: 19;
hence thesis by
A1,
XBOOLE_1: 48;
end;
theorem ::
UNIFORM3:39
for S be
Subset of (
partition_topology D) holds S is
open iff S is
closed by
Th18,
Th19;
registration
let X be non
empty
set, D be
a_partition of X;
cluster (
partition_topology D) -> non
empty;
coherence ;
end
theorem ::
UNIFORM3:40
for X be non
empty
set, D be
a_partition of X holds (
capOpCl (
partition_topology D))
= (
UniCl D)
proof
let X be non
empty
set, D be
a_partition of X;
set Y = { (A
/\ B) where A,B be
Subset of (
partition_topology D) : A is
open & B is
closed };
A1: Y
c= (
UniCl D)
proof
let x be
object;
assume x
in Y;
then
consider A,B be
Subset of (
partition_topology D) such that
A2: x
= (A
/\ B) and
A3: A is
open and
A4: B is
closed;
B is
open by
A4,
Th19;
hence thesis by
A2,
A3,
FINSUB_1:def 2;
end;
(
UniCl D)
c= Y
proof
let x be
object;
assume
A5: x
in (
UniCl D);
then
reconsider y = x as
Subset of (
partition_topology D);
X
in (
UniCl D) by
Th15;
then
reconsider XX = X as
Subset of (
partition_topology D);
A6: y
= (y
/\ X) by
XBOOLE_1: 18,
XBOOLE_1: 19;
y is
open & XX is
closed by
A5;
hence thesis by
A6;
end;
hence thesis by
A1;
end;
theorem ::
UNIFORM3:41
for X be non
empty
set, D be
a_partition of X holds (
OpenClosedSet (
partition_topology D))
= the
topology of (
partition_topology D)
proof
let X be non
empty
set, D be
a_partition of X;
thus (
OpenClosedSet (
partition_topology D))
c= the
topology of (
partition_topology D)
proof
let x be
object;
assume x
in (
OpenClosedSet (
partition_topology D));
then ex y be
Subset of (
partition_topology D) st x
= y & y is
open
closed;
hence thesis;
end;
let x be
object;
assume
A2: x
in the
topology of (
partition_topology D);
then
reconsider y = x as
Subset of (
partition_topology D);
y is
open by
A2;
then y is
open
closed by
Th18;
hence thesis;
end;
begin
reserve R for
Relation of X;
definition
let X be
set, R be
Relation of X;
::
UNIFORM3:def20
func
rho (R) -> non
empty
Subset-Family of
[:X, X:] equals { S where S be
Subset of
[:X, X:] : R
c= S };
coherence
proof
A1: R
in { S where S be
Subset of
[:X, X:] : R
c= S };
now
let x be
object;
assume x
in { S where S be
Subset of
[:X, X:] : R
c= S };
then ex S be
Subset of
[:X, X:] st x
= S & R
c= S;
hence x
in (
bool
[:X, X:]);
end;
then { S where S be
Subset of
[:X, X:] : R
c= S }
c= (
bool
[:X, X:]);
hence thesis by
A1;
end;
end
theorem ::
UNIFORM3:42
<.(
rho R).]
= (
rho R)
proof
<.(
rho R).]
c= (
rho R)
proof
let t be
object;
assume
A1: t
in
<.(
rho R).];
then
reconsider u = t as
Subset of
[:X, X:];
consider b be
Element of (
rho R) such that
A2: b
c= u by
A1,
CARDFIL2:def 8;
b
in (
rho R);
then ex c be
Subset of
[:X, X:] st b
= c & R
c= c;
then R
c= u by
A2;
hence thesis;
end;
hence thesis by
CARDFIL2: 18;
end;
theorem ::
UNIFORM3:43
<.
{R}.]
= (
rho R)
proof
thus
<.
{R}.]
c= (
rho R)
proof
let x be
object;
assume
A2: x
in
<.
{R}.];
then
reconsider y = x as
Subset of
[:X, X:];
consider b be
Element of
{R} such that
A3: b
c= y by
A2,
CARDFIL2:def 8;
R
c= y by
A3,
TARSKI:def 1;
hence thesis;
end;
let x be
object;
assume x
in (
rho R);
then
consider S be
Relation of X such that
A4: x
= S and
A5: R
c= S;
R is
Element of
{R} by
TARSKI:def 1;
hence thesis by
A4,
A5,
CARDFIL2:def 8;
end;
theorem ::
UNIFORM3:44
Th20: (
rho R) is
upper & (
rho R) is
cap-closed
proof
now
let Y1,Y2 be
Subset of
[:X, X:];
assume that
A1: Y1
in (
rho R) and
A2: Y1
c= Y2;
consider S be
Subset of
[:X, X:] such that
A3: Y1
= S and
A4: R
c= S by
A1;
R
c= Y2 by
A2,
A3,
A4;
hence Y2
in (
rho R);
end;
hence (
rho R) is
upper;
now
let X1,Y1 be
set;
assume that
A5: X1
in (
rho R) and
A6: Y1
in (
rho R);
consider SX be
Subset of
[:X, X:] such that
A7: X1
= SX and
A8: R
c= SX by
A5;
consider SY be
Subset of
[:X, X:] such that
A9: Y1
= SY and
A10: R
c= SY by
A6;
R
c= (SX
/\ SY) by
A8,
A10,
XBOOLE_1: 19;
hence (X1
/\ Y1)
in (
rho R) by
A7,
A9;
end;
hence (
rho R) is
cap-closed;
end;
registration
let X, R;
cluster (
rho R) ->
quasi_basis;
coherence
proof
now
let Y,Z be
Element of (
rho R);
Y
in (
rho R);
then
consider SY be
Subset of
[:X, X:] such that
A1: Y
= SY and
A2: R
c= SY;
Z
in (
rho R);
then
consider SZ be
Subset of
[:X, X:] such that
A3: Z
= SZ and
A4: R
c= SZ;
R
in (
rho R);
then
reconsider T = R as
Element of (
rho R);
T
c= (Y
/\ Z) by
A1,
A3,
A2,
A4,
XBOOLE_1: 19;
hence ex T be
Element of (
rho R) st T
c= (Y
/\ Z);
end;
hence thesis;
end;
end
theorem ::
UNIFORM3:45
Th21: for R be
total
reflexive
Relation of X holds (
rho R) is
axiom_UP1
proof
let R be
total
reflexive
Relation of X;
now
let B be
Element of (
rho R);
B
in (
rho R);
then
consider C be
Subset of
[:X, X:] such that
A1: B
= C and
A2: R
c= C;
A3: (
field R)
= X by
ORDERS_1: 12;
(
id X)
c= R
proof
let t be
object;
assume
A4: t
in (
id X);
then
consider a,b be
object such that a
in X and
A5: b
in X and
A6: t
=
[a, b] by
ZFMISC_1:def 2;
a
= b by
A4,
A6,
RELAT_1:def 10;
hence thesis by
A5,
A3,
A6,
RELAT_2:def 9,
RELAT_2:def 1;
end;
hence (
id X)
c= B by
A1,
A2;
end;
hence thesis;
end;
theorem ::
UNIFORM3:46
Th22: for R be
symmetric
Relation of X holds (
rho R) is
axiom_UP2
proof
let R be
symmetric
Relation of X;
let B1 be
Element of (
rho R);
B1
in (
rho R);
then
consider C1 be
Subset of
[:X, X:] such that
A1: B1
= C1 and
A2: R
c= C1;
reconsider R1 = C1 as
Relation of X;
A3: (R
~ )
c= (R1
~ ) by
A2,
SYSREL: 11;
R
in (
rho R);
then
reconsider B2 = R as
Element of (
rho R);
B2
c= (B1
~ ) by
A3,
A1,
RELAT_2: 13;
hence ex B2 be
Element of (
rho R) st B2
c= (B1
~ );
end;
theorem ::
UNIFORM3:47
Th24: for R be
total
transitive
Relation of X holds (
rho R) is
axiom_UP3
proof
let R be
total
transitive
Relation of X;
let B1 be
Element of (
rho R);
B1
in (
rho R);
then
consider C be
Subset of
[:X, X:] such that
A1: B1
= C and
A2: R
c= C;
R
in (
rho R);
then
reconsider B2 = R as
Element of (
rho R);
(R
* R)
c= R by
RELAT_2: 27;
then (B2
* B2)
c= B1 by
A1,
A2;
hence ex B2 be
Element of (
rho R) st (B2
* B2)
c= B1;
end;
definition
let X be
set, R be
Relation of X;
::
UNIFORM3:def21
func
uniformity_induced_by (R) ->
upper
cap-closed
strict
UniformSpaceStr equals
UniformSpaceStr (# X, (
rho R) #);
coherence
proof
UniformSpaceStr (# X, (
rho R) #) is
upper
cap-closed by
Th20;
hence thesis;
end;
end
theorem ::
UNIFORM3:48
Th25: for X be
set, R be
total
reflexive
Relation of X holds (
uniformity_induced_by R) is
axiom_U1
proof
let X be
set, R be
total
reflexive
Relation of X;
(
rho R) is
axiom_UP1 by
Th21;
hence thesis;
end;
theorem ::
UNIFORM3:49
Th26: for X be
set, R be
symmetric
Relation of X holds (
uniformity_induced_by R) is
axiom_U2
proof
let X be
set, R be
symmetric
Relation of X;
A1: (
rho R) is
axiom_UP2 by
Th22;
now
let S be
Element of the
entourages of (
uniformity_induced_by R);
reconsider S1 = S as
Element of (
rho R);
consider T be
Element of (
rho R) such that
A2: T
c= (S1
~ ) by
A1;
T
in (
rho R);
then
consider S2 be
Subset of
[:X, X:] such that
A3: T
= S2 and
A4: R
c= S2;
R
c= (S
[~] ) by
A2,
A3,
A4;
hence (S
[~] )
in the
entourages of (
uniformity_induced_by R);
end;
hence thesis;
end;
theorem ::
UNIFORM3:50
Th27: for X be
set, R be
total
transitive
Relation of X holds (
uniformity_induced_by R) is
axiom_U3
proof
let X be
set, R be
total
transitive
Relation of X;
A1: (
rho R) is
axiom_UP3 by
Th24;
let S be
Element of the
entourages of (
uniformity_induced_by R);
reconsider S1 = S as
Element of (
rho R);
consider W be
Element of (
rho R) such that
A2: (W
* W)
c= S1 by
A1;
thus ex W be
Element of the
entourages of (
uniformity_induced_by R) st (W
* W)
c= S by
A2;
end;
definition
let X be
set, R be
Tolerance of X;
:: original:
uniformity_induced_by
redefine
func
uniformity_induced_by (R) ->
strict
Semi-UniformSpace ;
coherence by
Th25,
Th26;
end
theorem ::
UNIFORM3:51
for X be
set, R be
Equivalence_Relation of X holds (
uniformity_induced_by R) is
UniformSpace by
Th27;
definition
let X be
set, R be
Equivalence_Relation of X;
:: original:
uniformity_induced_by
redefine
func
uniformity_induced_by (R) ->
strict
UniformSpace ;
coherence by
Th25,
Th26,
Th27;
end
registration
let X be non
empty
set, R be
Tolerance of X;
cluster (
uniformity_induced_by R) -> non
empty;
coherence ;
end
registration
cluster ->
topological for non
empty
UniformSpace;
coherence ;
end
definition
let US be non
empty
UniformSpace;
::
UNIFORM3:def22
func
@ US ->
topological non
empty
axiom_U1
UniformSpaceStr equals US;
coherence ;
end
theorem ::
UNIFORM3:52
for X be non
empty
set, R be
Equivalence_Relation of X holds (
TopSpace_induced_by (
@ (
uniformity_induced_by R)))
= (
partition_topology (
Class R))
proof
let X be non
empty
set, R be
Equivalence_Relation of X;
set T1 = (
TopSpace_induced_by (
@ (
uniformity_induced_by R))), T2 = (
partition_topology (
Class R));
now
thus the
carrier of T1
= the
carrier of T2 by
FINTOPO7:def 16;
A1: the
topology of T1
= (
Family_open_set (
FMT_induced_by (
@ (
uniformity_induced_by R)))) by
FINTOPO7:def 16
.= the set of all O where O be
open
Subset of (
FMT_induced_by (
@ (
uniformity_induced_by R)));
A2: the
topology of T2
= the set of all (
union P) where P be
Subset of (
Class R) by
Th14;
A3: the
topology of T1
c= the
topology of T2
proof
let t be
object;
assume t
in the
topology of T1;
then
consider O be
open
Subset of (
FMT_induced_by (
@ (
uniformity_induced_by R))) such that
A4: t
= O by
A1;
per cases ;
suppose
A5: O is
empty;
{}
c= (
Class R);
then
reconsider P =
{} as
Subset of (
Class R);
t
= (
union P) by
A4,
A5,
ZFMISC_1: 2;
hence thesis by
A2;
end;
suppose
A6: O is non
empty;
set P = the set of all (
Class (R,u)) where u be
Element of O;
P
c= (
Class R)
proof
let u be
object;
assume u
in P;
then
consider u0 be
Element of O such that
A7: u
= (
Class (R,u0));
A8: u0
in O by
A6;
thus thesis by
A7,
A8,
EQREL_1:def 3;
end;
then
reconsider P as
Subset of (
Class R);
reconsider t1 = t as
Subset of X by
A4;
t1
= (
union P)
proof
thus t1
c= (
union P)
proof
let a be
object;
assume
A10: a
in t1;
then
reconsider b = a as
Element of O by
A4;
b
in (
Class (R,b)) & (
Class (R,b))
in P by
A10,
EQREL_1: 20;
hence thesis by
TARSKI:def 4;
end;
let a be
object;
assume a
in (
union P);
then
consider Q be
set such that
A11: a
in Q and
A12: Q
in P by
TARSKI:def 4;
consider v be
Element of O such that
A13: Q
= (
Class (R,v)) by
A12;
v
in O by
A6;
then
reconsider w = v as
Element of (
@ (
uniformity_induced_by R));
O
in (
Neighborhood w) by
Th8,
A6;
then
consider V be
Element of the
entourages of (
@ (
uniformity_induced_by R)) such that
A14: O
= (
Neighborhood (V,w));
V
in (
rho R);
then
consider W be
Relation of the
carrier of (
@ (
uniformity_induced_by R)) such that
A15: V
= W and
A16: R
c= W;
A17: (
Neighborhood (V,w))
= (V
.:
{w}) & (
Neighborhood (V,w))
= (
rng (V
|
{w})) & (
Neighborhood (V,w))
= (
Im (V,w)) & (
Neighborhood (V,w))
= (
Class (V,w)) & (
Neighborhood (V,w))
= (
neighbourhood (w,V)) by
UNIFORM2: 14;
(
Class (R,w))
c= (
Class (W,w))
proof
let z be
object;
assume z
in (
Class (R,w));
then
[w, z]
in W by
A16,
EQREL_1: 18;
hence thesis by
EQREL_1: 18;
end;
hence thesis by
A11,
A13,
A4,
A17,
A15,
A14;
end;
hence thesis by
A2;
end;
end;
the
topology of T2
c= the
topology of T1
proof
let t be
object;
assume
A18: t
in the
topology of T2;
then
consider P be
Subset of (
Class R) such that
A19: t
= (
union P) by
A2;
reconsider Q = (
union P) as
Subset of (
FMT_induced_by (
@ (
uniformity_induced_by R))) by
A18,
A19;
for x be
Element of (
@ (
uniformity_induced_by R)) st x
in Q holds Q
in (
Neighborhood x)
proof
let x be
Element of (
@ (
uniformity_induced_by R));
assume
A20: x
in Q;
then
consider T be
set such that
A21: x
in T and
A22: T
in P by
TARSKI:def 4;
T
in (
Class R) by
A22;
then
consider b be
object such that
A23: b
in X and
A24: T
= (
Class (R,b)) by
EQREL_1:def 3;
set S1 = the set of all
[x, y] where y be
Element of Q;
set S = (R
\/ S1);
S1
c=
[:X, X:]
proof
let s be
object;
assume s
in S1;
then
consider y be
Element of Q such that
A25: s
=
[x, y];
Q
c= X;
then y
in X by
A20;
hence thesis by
A25,
ZFMISC_1:def 2;
end;
then
reconsider S as
Subset of
[:X, X:] by
XBOOLE_1: 8;
R
c= S by
XBOOLE_1: 7;
then S
in (
rho R);
then
reconsider V = S as
Element of the
entourages of (
@ (
uniformity_induced_by R));
Q
= (
Neighborhood (V,x))
proof
thus Q
c= (
Neighborhood (V,x))
proof
let a be
object;
assume a
in Q;
then
reconsider b = a as
Element of Q;
A27:
[x, b]
in S1;
A28: S1
c= (R
\/ S1) by
XBOOLE_1: 7;
b
in Q by
A20;
then
reconsider c = b as
Element of (
@ (
uniformity_induced_by R));
[x, c]
in V by
A28,
A27;
hence thesis;
end;
let a be
object;
assume a
in (
Neighborhood (V,x));
then
consider y be
Element of (
@ (
uniformity_induced_by R)) such that
A29: a
= y and
A30:
[x, y]
in V;
per cases by
A29,
A30,
XBOOLE_0:def 3;
suppose
[x, a]
in S1;
then
consider y be
Element of Q such that
A31:
[x, a]
=
[x, y];
a
= y by
A31,
XTUPLE_0: 1;
hence thesis by
A20;
end;
suppose
[x, a]
in R;
then
A32: a
in (
Class (R,x)) by
EQREL_1: 18;
(
Class (R,b))
= (
Class (R,x)) by
A21,
A23,
A24,
EQREL_1: 23;
hence thesis by
A22,
A24,
A32,
TARSKI:def 4;
end;
end;
hence thesis;
end;
then
reconsider O = (
union P) as
open
Subset of (
FMT_induced_by (
@ (
uniformity_induced_by R))) by
Th8;
t
= O by
A19;
hence thesis by
A1;
end;
hence the
topology of T1
= the
topology of T2 by
A3;
end;
hence thesis;
end;
begin
theorem ::
UNIFORM3:53
for USS be
upper
UniformSpaceStr st (
meet the
entourages of USS)
in the
entourages of USS holds ex R be
Relation of the
carrier of USS st (
meet the
entourages of USS)
= R & the
entourages of USS
= (
rho R)
proof
let USS be
upper
UniformSpaceStr;
assume
A1: (
meet the
entourages of USS)
in the
entourages of USS;
reconsider R = (
meet the
entourages of USS) as
Relation of the
carrier of USS;
take R;
A2: (
rho R)
c= the
entourages of USS
proof
let x be
object;
assume x
in (
rho R);
then
consider S be
Subset of
[:the
carrier of USS, the
carrier of USS:] such that
A3: x
= S and
A4: R
c= S;
the
entourages of USS is
upper by
UNIFORM2:def 7;
hence thesis by
A1,
A3,
A4;
end;
the
entourages of USS
c= (
rho R)
proof
let x be
object;
assume x
in the
entourages of USS;
then
consider S be
Subset of
[:the
carrier of USS, the
carrier of USS:] such that
A5: x
= S and
A6: S
in the
entourages of USS;
R
c= S by
A6,
SETFAM_1: 3;
hence thesis by
A5;
end;
hence thesis by
A2;
end;
definition
let USS be
UniformSpaceStr;
::
UNIFORM3:def23
func
Uniformity2InternalRel (USS) ->
Relation of the
carrier of USS equals (
meet the
entourages of USS);
coherence ;
end
definition
let USS be
UniformSpaceStr;
::
UNIFORM3:def24
func
UniformSpaceStr2RelStr (USS) ->
RelStr equals
RelStr (# the
carrier of USS, (
Uniformity2InternalRel USS) #);
coherence ;
end
definition
let RS be
RelStr;
::
UNIFORM3:def25
func
InternalRel2Uniformity (RS) ->
Subset-Family of
[:the
carrier of RS, the
carrier of RS:] equals { R where R be
Relation of the
carrier of RS : the
InternalRel of RS
c= R };
coherence
proof
set IRS = { R where R be
Relation of the
carrier of RS : the
InternalRel of RS
c= R };
IRS
c= (
bool
[:the
carrier of RS, the
carrier of RS:])
proof
let x be
object;
assume x
in IRS;
then ex R be
Relation of the
carrier of RS st x
= R & the
InternalRel of RS
c= R;
hence thesis;
end;
hence thesis;
end;
end
definition
let RS be
RelStr;
::
UNIFORM3:def26
func
RelStr2UniformSpaceStr (RS) ->
strict
UniformSpaceStr equals
UniformSpaceStr (# the
carrier of RS, (
InternalRel2Uniformity RS) #);
coherence ;
end
definition
let RS be
RelStr;
::
UNIFORM3:def27
func
InternalRel2Element (RS) ->
Element of the
entourages of (
RelStr2UniformSpaceStr RS) equals the
InternalRel of RS;
coherence
proof
the
InternalRel of RS
in the
entourages of (
RelStr2UniformSpaceStr RS);
hence thesis;
end;
end
theorem ::
UNIFORM3:54
Th28: for R be
Relation of X holds (
meet (
rho R))
= R
proof
let R be
Relation of X;
thus (
meet (
rho R))
c= R
proof
let x be
object;
assume
A2: x
in (
meet (
rho R));
R
in (
rho R);
hence thesis by
A2,
SETFAM_1:def 1;
end;
let x be
object;
assume
A3: x
in R;
now
let Y be
set;
assume Y
in (
rho R);
then ex S be
Relation of X st Y
= S & R
c= S;
hence x
in Y by
A3;
end;
hence thesis by
SETFAM_1:def 1;
end;
theorem ::
UNIFORM3:55
for RS be
strict
RelStr holds (
UniformSpaceStr2RelStr (
RelStr2UniformSpaceStr RS))
= RS
proof
let RS be
strict
RelStr;
set US = (
UniformSpaceStr2RelStr (
RelStr2UniformSpaceStr RS));
now
thus the
carrier of US
= the
carrier of RS;
the
InternalRel of US
= (
meet (
rho the
InternalRel of RS));
hence the
InternalRel of US
= the
InternalRel of RS by
Th28;
end;
hence thesis;
end;
theorem ::
UNIFORM3:56
for US be
UniformSpaceStr holds the
carrier of (
RelStr2UniformSpaceStr (
UniformSpaceStr2RelStr US))
= the
carrier of US & the
entourages of (
RelStr2UniformSpaceStr (
UniformSpaceStr2RelStr US))
= (
rho (
meet the
entourages of US));
theorem ::
UNIFORM3:57
Th29: for SF be
Subset-Family of
[:X, X:], R be
Relation of X st SF
= (
rho R) holds SF
c= (
rho (
meet SF))
proof
let SF be
Subset-Family of
[:X, X:], R be
Relation of X;
assume
A1: SF
= (
rho R);
SF
c= (
rho (
meet SF))
proof
let x be
object;
assume
A2: x
in SF;
then
consider S be
Subset of
[:X, X:] such that
A3: x
= S and R
c= S by
A1;
(
meet SF)
c= S by
A3,
A2,
SETFAM_1:def 1;
hence thesis by
A3;
end;
hence thesis;
end;
theorem ::
UNIFORM3:58
Th30: for SF be
upper
Subset-Family of
[:X, X:] st (
meet SF)
in SF holds (
rho (
meet SF))
c= SF
proof
let SF be
upper
Subset-Family of
[:X, X:];
assume
A1: (
meet SF)
in SF;
thus (
rho (
meet SF))
c= SF
proof
let x be
object;
assume x
in (
rho (
meet SF));
then
consider S be
Subset of
[:X, X:] such that
A2: x
= S and
A3: (
meet SF)
c= S;
SF is
upper;
hence thesis by
A2,
A3,
A1;
end;
thus thesis;
end;
theorem ::
UNIFORM3:59
for SF be
upper
Subset-Family of
[:X, X:], R be
Relation of X st R
in SF & SF
= (
rho R) & (
meet SF)
in SF holds (
rho (
meet SF))
= SF by
Th29,
Th30;
theorem ::
UNIFORM3:60
Th31: for US be
upper
UniformSpaceStr st ex R be
Relation of the
carrier of US st the
entourages of US
= (
rho R) & (
meet the
entourages of US)
in the
entourages of US holds the
entourages of US
= (
rho (
meet the
entourages of US))
proof
let US be
upper
UniformSpaceStr;
given R be
Relation of the
carrier of US such that
A2: the
entourages of US
= (
rho R) and
A3: (
meet the
entourages of US)
in the
entourages of US;
the
entourages of US is
upper by
UNIFORM2:def 7;
hence thesis by
A2,
A3,
Th29,
Th30;
end;
theorem ::
UNIFORM3:61
for US be
upper
UniformSpaceStr, R be
Relation of the
carrier of US st the
entourages of US
= (
rho R) & (
meet the
entourages of US)
in the
entourages of US holds the
entourages of US
= (
rho (
meet the
entourages of US)) by
Th31;
theorem ::
UNIFORM3:62
for R be
Tolerance of X holds (
uniformity_induced_by R) is
Semi-UniformSpace & the
entourages of (
uniformity_induced_by R)
= (
rho R) & (
meet the
entourages of (
uniformity_induced_by R))
= R by
Th28;
theorem ::
UNIFORM3:63
for R be
Tolerance of X holds (
RelStr2UniformSpaceStr (
UniformSpaceStr2RelStr (
uniformity_induced_by R)))
= (
uniformity_induced_by R)
proof
let R be
Tolerance of X;
the
carrier of (
RelStr2UniformSpaceStr (
UniformSpaceStr2RelStr (
uniformity_induced_by R)))
= the
carrier of (
uniformity_induced_by R) & the
entourages of (
RelStr2UniformSpaceStr (
UniformSpaceStr2RelStr (
uniformity_induced_by R)))
= (
rho (
meet the
entourages of (
uniformity_induced_by R)));
hence thesis by
Th28;
end;
theorem ::
UNIFORM3:64
for R be
Equivalence_Relation of X holds (
RelStr2UniformSpaceStr (
UniformSpaceStr2RelStr (
uniformity_induced_by R)))
= (
uniformity_induced_by R)
proof
let R be
Equivalence_Relation of X;
the
carrier of (
RelStr2UniformSpaceStr (
UniformSpaceStr2RelStr (
uniformity_induced_by R)))
= the
carrier of (
uniformity_induced_by R) & the
entourages of (
RelStr2UniformSpaceStr (
UniformSpaceStr2RelStr (
uniformity_induced_by R)))
= (
rho (
meet the
entourages of (
uniformity_induced_by R)));
hence thesis by
Th28;
end;
begin
definition
let X be
set, SF be
Subset-Family of X, A be
Element of SF;
::
UNIFORM3:def28
func
block_Pervin_uniformity (A) ->
Subset of
[:X, X:] equals (
[:(X
\ A), (X
\ A):]
\/
[:A, A:]);
coherence
proof
per cases ;
suppose SF is
empty;
then A is
empty by
SUBSET_1:def 1;
then
[:A, A:]
c=
[:X, X:];
hence thesis by
XBOOLE_1: 8;
end;
suppose SF is non
empty;
then A
in SF;
then
[:A, A:]
c=
[:X, X:] by
ZFMISC_1: 96;
hence thesis by
XBOOLE_1: 8;
end;
end;
end
reserve SF for
Subset-Family of X,
A for
Element of SF;
theorem ::
UNIFORM3:65
Th34: A
=
{} implies (
block_Pervin_uniformity A)
=
[:X, X:]
proof
assume A
=
{} ;
then (
block_Pervin_uniformity A)
= (
[:(X
\
{} ), (X
\
{} ):]
\/
[:
{} ,
{} :]);
hence thesis;
end;
theorem ::
UNIFORM3:66
X is non
empty implies (
block_Pervin_uniformity A)
= {
[x, y] where x,y be
Element of X : x
in A iff y
in A }
proof
assume
A1: X is non
empty;
set S = {
[x, y] where x,y be
Element of X : x
in A iff y
in A };
A2: (
block_Pervin_uniformity A)
c= S
proof
let x be
object;
assume
A3: x
in (
block_Pervin_uniformity A);
then
A4: x
in
[:A, A:] or x
in
[:(X
\ A), (X
\ A):] by
XBOOLE_0:def 3;
consider a,b be
object such that
A9: a
in X and
A10: b
in X and
A11: x
=
[a, b] by
A3,
ZFMISC_1:def 2;
(a
in A & b
in A) or (a
in (X
\ A) & b
in (X
\ A)) by
A4,
A11,
ZFMISC_1: 87;
then (a
in A & b
in A) or ((a
in X & not a
in A) & (b
in X & not b
in A)) by
XBOOLE_0:def 5;
hence thesis by
A9,
A10,
A11;
end;
S
c= (
block_Pervin_uniformity A)
proof
let x be
object;
assume x
in S;
then
consider a,b be
Element of X such that
A12: x
=
[a, b] and
A13: a
in A iff b
in A;
x
in
[:A, A:] or (a
in (X
\ A) & b
in (X
\ A)) by
A1,
A13,
A12,
ZFMISC_1: 87,
XBOOLE_0:def 5;
then x
in
[:A, A:] or x
in
[:(X
\ A), (X
\ A):] by
A12,
ZFMISC_1: 87;
hence thesis by
XBOOLE_0:def 3;
end;
hence thesis by
A2;
end;
theorem ::
UNIFORM3:67
Th35: (
id X)
c= (
block_Pervin_uniformity A) & ((
block_Pervin_uniformity A)
* (
block_Pervin_uniformity A))
c= (
block_Pervin_uniformity A)
proof
thus (
id X)
c= (
block_Pervin_uniformity A)
proof
let t be
object;
assume
A1: t
in (
id X);
then
consider a,b be
object such that
A2: t
=
[a, b] by
RELAT_1:def 1;
A3: a
in X & a
= b by
A1,
A2,
RELAT_1:def 10;
per cases ;
suppose a
in A;
then a
in A & b
in A by
A1,
A2,
RELAT_1:def 10;
then
[a, b]
in
[:A, A:] by
ZFMISC_1:def 2;
hence thesis by
A2,
XBOOLE_0:def 3;
end;
suppose not a
in A;
then a
in (X
\ A) by
A3,
XBOOLE_0:def 5;
then t
in
[:(X
\ A), (X
\ A):] by
A2,
A3,
ZFMISC_1:def 2;
hence thesis by
XBOOLE_0:def 3;
end;
end;
now
let t be
object;
assume
A4: t
in ((
block_Pervin_uniformity A)
* (
block_Pervin_uniformity A));
then
consider a,b be
object such that
A5: t
=
[a, b] by
RELAT_1:def 1;
[a, b]
in {
[x, y] where x,y be
Element of X : ex z be
Element of X st
[x, z]
in (
block_Pervin_uniformity A) &
[z, y]
in (
block_Pervin_uniformity A) } by
A5,
A4,
UNIFORM2: 3;
then
consider x,y be
Element of X such that
A6:
[a, b]
=
[x, y] and
A7: ex z be
Element of X st
[x, z]
in (
block_Pervin_uniformity A) &
[z, y]
in (
block_Pervin_uniformity A);
consider z be
Element of X such that
A8:
[x, z]
in (
block_Pervin_uniformity A) and
A9:
[z, y]
in (
block_Pervin_uniformity A) by
A7;
per cases ;
suppose
A10: x
in A;
[x, z]
in
[:A, A:]
proof
per cases by
A8,
XBOOLE_0:def 3;
suppose
[x, z]
in
[:(X
\ A), (X
\ A):];
then x
in (X
\ A) by
ZFMISC_1: 87;
hence thesis by
A10,
XBOOLE_0:def 5;
end;
suppose
[x, z]
in
[:A, A:];
hence thesis;
end;
end;
then
A11: z
in A by
ZFMISC_1: 87;
[z, y]
in
[:A, A:]
proof
per cases by
A9,
XBOOLE_0:def 3;
suppose
[z, y]
in
[:(X
\ A), (X
\ A):];
then z
in (X
\ A) & y
in X by
ZFMISC_1: 87;
hence thesis by
A11,
XBOOLE_0:def 5;
end;
suppose
[z, y]
in
[:A, A:];
hence thesis;
end;
end;
then y
in A by
ZFMISC_1: 87;
then
[x, y]
in
[:A, A:] by
A10,
ZFMISC_1:def 2;
hence t
in (
block_Pervin_uniformity A) by
A5,
A6,
XBOOLE_0:def 3;
end;
suppose
A12: not x
in A;
per cases ;
suppose X is
empty;
hence t
in (
block_Pervin_uniformity A) by
A9;
end;
suppose X is non
empty;
then
A13: x
in (X
\ A) by
A12,
XBOOLE_0:def 5;
[x, z]
in
[:(X
\ A), (X
\ A):]
proof
per cases by
A8,
XBOOLE_0:def 3;
suppose
[x, z]
in
[:(X
\ A), (X
\ A):];
hence thesis;
end;
suppose
[x, z]
in
[:A, A:];
hence thesis by
A12,
ZFMISC_1: 87;
end;
end;
then
A14: z
in (X
\ A) by
ZFMISC_1: 87;
[z, y]
in
[:(X
\ A), (X
\ A):]
proof
per cases by
A9,
XBOOLE_0:def 3;
suppose
[z, y]
in
[:(X
\ A), (X
\ A):];
hence thesis;
end;
suppose
[z, y]
in
[:A, A:];
then z
in A & y
in A by
ZFMISC_1: 87;
hence thesis by
A14,
XBOOLE_0:def 5;
end;
end;
then y
in (X
\ A) by
ZFMISC_1: 87;
then
[x, y]
in
[:(X
\ A), (X
\ A):] by
A13,
ZFMISC_1:def 2;
hence t
in (
block_Pervin_uniformity A) by
A5,
A6,
XBOOLE_0:def 3;
end;
end;
end;
hence thesis;
end;
definition
let X be
set, SF be
Subset-Family of X;
::
UNIFORM3:def29
func
subbasis_Pervin_uniformity (SF) ->
Subset-Family of
[:X, X:] equals the set of all (
block_Pervin_uniformity A) where A be
Element of SF;
coherence
proof
the set of all (
block_Pervin_uniformity A) where A be
Element of SF
c= (
bool
[:X, X:])
proof
let x be
object;
assume x
in the set of all (
block_Pervin_uniformity A) where A be
Element of SF;
then
consider A be
Element of SF such that
A1: x
= (
block_Pervin_uniformity A);
thus thesis by
A1;
end;
hence thesis;
end;
end
registration
let X be
set, SF be
Subset-Family of X;
cluster (
subbasis_Pervin_uniformity SF) -> non
empty;
coherence
proof
set A = the
Element of SF;
set S = (
block_Pervin_uniformity A);
S
in (
subbasis_Pervin_uniformity SF);
hence thesis;
end;
end
definition
let X be
set, SF be
Subset-Family of X;
::
UNIFORM3:def30
func
basis_Pervin_uniformity (SF) ->
Subset-Family of
[:X, X:] equals (
FinMeetCl (
subbasis_Pervin_uniformity SF));
coherence ;
end
theorem ::
UNIFORM3:68
Th36: (
basis_Pervin_uniformity SF) is
cap-closed
proof
now
let x,y be
set;
assume that
A1: x
in (
basis_Pervin_uniformity SF) and
A2: y
in (
basis_Pervin_uniformity SF);
consider Y be
Subset-Family of
[:X, X:] such that
A3: Y
c= (
subbasis_Pervin_uniformity SF) and
A4: Y is
finite and
A5: x
= (
Intersect Y) by
A1,
CANTOR_1:def 3;
consider Z be
Subset-Family of
[:X, X:] such that
A6: Z
c= (
subbasis_Pervin_uniformity SF) and
A7: Z is
finite and
A8: y
= (
Intersect Z) by
A2,
CANTOR_1:def 3;
A9: (x
/\ y)
= (
Intersect (Y
\/ Z)) by
A5,
A8,
MSSUBFAM: 8;
(Y
\/ Z)
c= (
subbasis_Pervin_uniformity SF) by
A3,
A6,
XBOOLE_1: 8;
hence (x
/\ y)
in (
basis_Pervin_uniformity SF) by
A9,
A4,
A7,
CANTOR_1:def 3;
end;
hence thesis;
end;
theorem ::
UNIFORM3:69
Th37: (
basis_Pervin_uniformity SF) is
quasi_basis
proof
(
basis_Pervin_uniformity SF) is
cap-closed by
Th36;
hence thesis;
end;
theorem ::
UNIFORM3:70
Th38: (
basis_Pervin_uniformity SF) is
axiom_UP1
proof
for B be
Element of (
basis_Pervin_uniformity SF) holds (
id X)
c= B
proof
let B be
Element of (
basis_Pervin_uniformity SF);
B
in (
FinMeetCl (
subbasis_Pervin_uniformity SF));
then
consider Y be
Subset-Family of
[:X, X:] such that
A1: Y
c= (
subbasis_Pervin_uniformity SF) and Y is
finite and
A2: B
= (
Intersect Y) by
CANTOR_1:def 3;
(
id X)
c= B
proof
let t be
object;
assume
A3: t
in (
id X);
then
consider a,b be
object such that
A4: t
=
[a, b] by
RELAT_1:def 1;
A5: a
in X & a
= b by
A3,
A4,
RELAT_1:def 10;
per cases ;
suppose Y is
empty;
then B
=
[:X, X:] by
A2,
SETFAM_1:def 9;
hence thesis by
A3;
end;
suppose
A7: Y is non
empty;
then
A8: (
Intersect Y)
= (
meet Y) by
SETFAM_1:def 9;
now
let y be
set;
assume y
in Y;
then y
in the set of all (
block_Pervin_uniformity O) where O be
Element of SF by
A1;
then
consider O be
Element of SF such that
A9: y
= (
block_Pervin_uniformity O);
A10:
[:(X
\ O), (X
\ O):]
c= y &
[:O, O:]
c= y by
A9,
XBOOLE_1: 10;
per cases by
A5,
XBOOLE_0:def 5;
suppose a
in (X
\ O);
then
[a, b]
in
[:(X
\ O), (X
\ O):] by
A5,
ZFMISC_1:def 2;
hence t
in y by
A4,
A10;
end;
suppose a
in O;
then
[a, b]
in
[:O, O:] by
A5,
ZFMISC_1:def 2;
hence t
in y by
A4,
A10;
end;
end;
hence thesis by
A2,
A8,
A7,
SETFAM_1:def 1;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem ::
UNIFORM3:71
Th39: for A be
Element of SF, R be
Relation of X st R
= (
block_Pervin_uniformity A) holds (R
~ )
= (
block_Pervin_uniformity A)
proof
let A be
Element of SF, R be
Relation of X;
assume
A1: R
= (
block_Pervin_uniformity A);
per cases ;
suppose SF is
empty;
then
F1: A
=
{} by
SUBSET_1:def 1;
then R
=
[:X, X:] by
A1,
Th34;
then (R
~ )
=
[:X, X:] by
SYSREL: 5;
hence thesis by
F1,
Th34;
end;
suppose SF is non
empty;
then A
in SF;
then
reconsider A as
Subset of X;
(R
~ )
= (
[:A, A:]
\/
[:(X
\ A), (X
\ A):]) by
A1,
Th33;
hence thesis;
end;
end;
theorem ::
UNIFORM3:72
for R be
Relation of X st R is
Element of (
subbasis_Pervin_uniformity SF) holds (R
~ ) is
Element of (
subbasis_Pervin_uniformity SF)
proof
let R be
Relation of X;
assume
A1: R is
Element of (
subbasis_Pervin_uniformity SF);
then R
in the set of all (
block_Pervin_uniformity A) where A be
Element of SF;
then ex A be
Element of SF st R
= (
block_Pervin_uniformity A);
hence thesis by
A1,
Th39;
end;
theorem ::
UNIFORM3:73
Th40: for Y be non
empty
Subset-Family of
[:X, X:] st Y
c= (
subbasis_Pervin_uniformity SF) holds (Y
[~] )
= Y
proof
let Y be non
empty
Subset-Family of
[:X, X:];
assume
A1: Y
c= (
subbasis_Pervin_uniformity SF);
A2: (Y
[~] )
c= Y
proof
let x be
object;
assume x
in (Y
[~] );
then
consider y be
Element of Y such that
A3: x
= (y
~ );
y
in (
subbasis_Pervin_uniformity SF) by
A1;
then
consider A be
Element of SF such that
A4: y
= (
block_Pervin_uniformity A);
reconsider z = y as
Relation of X;
(z
~ )
= y by
A4,
Th39;
hence thesis by
A3;
end;
Y
c= (Y
[~] )
proof
let x be
object;
assume x
in Y;
then
consider y be
Element of Y such that
A5: x
= y;
y
in (
subbasis_Pervin_uniformity SF) by
A1;
then
consider A be
Element of SF such that
A6: y
= (
block_Pervin_uniformity A);
reconsider z = y as
Relation of X;
reconsider t = (z
~ ) as
Element of Y by
A6,
Th39;
(t
~ )
in (Y
[~] );
hence thesis by
A5;
end;
hence thesis by
A2;
end;
theorem ::
UNIFORM3:74
Th41: for Y be non
empty
Subset-Family of
[:X, X:] st Y
c= (
subbasis_Pervin_uniformity SF) holds ((
meet Y)
~ )
= (
meet (Y
[~] ))
proof
let Y be non
empty
Subset-Family of
[:X, X:];
assume
A1: Y
c= (
subbasis_Pervin_uniformity SF);
thus ((
meet Y)
~ )
c= (
meet (Y
[~] ))
proof
let x be
object;
assume
A3: x
in ((
meet Y)
~ );
then
consider a,b be
object such that a
in X and b
in X and
A4:
[a, b]
= x by
ZFMISC_1:def 2;
A5:
[b, a]
in (
meet Y) by
A3,
A4,
RELAT_1:def 7;
Y is non
empty;
then
consider y be
object such that
A6: y
in Y;
reconsider y as
Element of Y by
A6;
reconsider z = y as
Relation of X;
A7: (y
~ )
in (Y
[~] );
now
let Z be
set;
assume
A8: Z
in (Y
[~] );
then
A9: Z
in Y by
A1,
Th40;
reconsider T = Z as
Relation of X by
A8;
T
in (
subbasis_Pervin_uniformity SF) by
A9,
A1;
then
consider A be
Element of SF such that
A10: T
= (
block_Pervin_uniformity A);
(T
~ )
= T by
A10,
Th39;
then
[b, a]
in (T
~ ) by
A9,
A5,
SETFAM_1:def 1;
hence
[a, b]
in Z by
RELAT_1:def 7;
end;
hence thesis by
A7,
A4,
SETFAM_1:def 1;
end;
let x be
object;
assume
A11: x
in (
meet (Y
[~] ));
then
consider a,b be
object such that a
in X and b
in X and
A12:
[a, b]
= x by
ZFMISC_1:def 2;
now
let Z be
set;
assume
A13: Z
in Y;
then
reconsider T = Z as
Relation of X;
reconsider R = T as
Element of Y by
A13;
(R
~ )
= (T
~ );
then (T
~ )
in (Y
[~] );
then
[a, b]
in (T
~ ) by
A11,
A12,
SETFAM_1:def 1;
hence
[b, a]
in Z by
RELAT_1:def 7;
end;
then
[b, a]
in (
meet Y) by
SETFAM_1:def 1;
hence thesis by
A12,
RELAT_1:def 7;
end;
theorem ::
UNIFORM3:75
Th42: for Y be non
empty
Subset-Family of
[:X, X:] st Y
c= (
subbasis_Pervin_uniformity SF) holds (
meet Y)
= ((
meet Y)
~ )
proof
let Y be non
empty
Subset-Family of
[:X, X:];
assume
A1: Y
c= (
subbasis_Pervin_uniformity SF);
then (
meet (Y
[~] ))
= (
meet Y) by
Th40;
hence thesis by
A1,
Th41;
end;
theorem ::
UNIFORM3:76
Th43: (
basis_Pervin_uniformity SF) is
axiom_UP2
proof
let B1 be
Element of (
basis_Pervin_uniformity SF);
B1
in (
FinMeetCl (
subbasis_Pervin_uniformity SF));
then
consider Y be
Subset-Family of
[:X, X:] such that
A1: Y
c= (
subbasis_Pervin_uniformity SF) and Y is
finite and
A2: B1
= (
Intersect Y) by
CANTOR_1:def 3;
per cases ;
suppose Y is
empty;
then
A3: B1
=
[:X, X:] by
A2,
SETFAM_1:def 9;
B1
c= (B1
~ )
proof
let x be
object;
assume x
in B1;
then
consider a,b be
object such that
A4: a
in X and
A5: b
in X and
A6: x
=
[a, b] by
A2,
ZFMISC_1:def 2;
[b, a]
in B1 by
A3,
A4,
A5,
ZFMISC_1:def 2;
hence thesis by
A6,
RELAT_1:def 7;
end;
hence thesis;
end;
suppose
A9: Y is non
empty;
then
A10: B1
= (
meet Y) by
A2,
SETFAM_1:def 9;
set Y2 = (Y
[~] );
(Y
[~] )
= Y by
A1,
A9,
Th40;
then
reconsider B2 = (
meet Y2) as
Element of (
basis_Pervin_uniformity SF) by
A9,
A2,
SETFAM_1:def 9;
B2
c= (B1
~ )
proof
let x be
object;
assume x
in B2;
then x
in (
meet Y) by
A1,
A9,
Th40;
hence thesis by
A10,
A1,
A9,
Th42;
end;
hence thesis;
end;
end;
theorem ::
UNIFORM3:77
Th44: (
basis_Pervin_uniformity SF) is
axiom_UP3
proof
for B1 be
Element of (
basis_Pervin_uniformity SF) holds ex B2 be
Element of (
basis_Pervin_uniformity SF) st (B2
[*] B2)
c= B1
proof
let B1 be
Element of (
basis_Pervin_uniformity SF);
B1
in (
FinMeetCl (
subbasis_Pervin_uniformity SF));
then
consider Y be
Subset-Family of
[:X, X:] such that
A1: Y
c= (
subbasis_Pervin_uniformity SF) and Y is
finite and
A2: B1
= (
Intersect Y) by
CANTOR_1:def 3;
per cases ;
suppose Y is
empty;
then
A3: B1
=
[:X, X:] by
A2,
SETFAM_1:def 9;
take B1;
thus thesis by
A3;
end;
suppose
A4: Y is non
empty;
then
A5: B1
= (
meet Y) by
A2,
SETFAM_1:def 9;
reconsider B2 = B1 as
Element of (
basis_Pervin_uniformity SF);
take B2;
(B2
* B2)
c= B1
proof
let t be
object;
assume
A6: t
in (B2
* B2);
then
consider a,b be
object such that
A10: t
=
[a, b] by
RELAT_1:def 1;
consider c be
object such that
A11:
[a, c]
in B1 and
A12:
[c, b]
in B1 by
A6,
A10,
RELAT_1:def 8;
t
in B1
proof
for Z be
set st Z
in Y holds t
in Z
proof
let Z be
set;
assume
A13: Z
in Y;
then Z
in the set of all (
block_Pervin_uniformity O) where O be
Element of SF by
A1;
then
consider O be
Element of SF such that
A14: Z
= (
block_Pervin_uniformity O);
[a, c]
in (
meet Y) by
A4,
A2,
SETFAM_1:def 9,
A11;
then
A15:
[a, c]
in (
block_Pervin_uniformity O) by
A14,
A13,
SETFAM_1:def 1;
[c, b]
in (
block_Pervin_uniformity O) by
A12,
A5,
A14,
A13,
SETFAM_1:def 1;
then
A16:
[a, b]
in ((
block_Pervin_uniformity O)
* (
block_Pervin_uniformity O)) by
A15,
RELAT_1:def 8;
((
block_Pervin_uniformity O)
* (
block_Pervin_uniformity O))
c= (
block_Pervin_uniformity O) by
Th35;
hence thesis by
A14,
A10,
A16;
end;
hence thesis by
A5,
A4,
SETFAM_1:def 1;
end;
hence thesis;
end;
hence thesis;
end;
end;
hence thesis;
end;
Th45: ex US be
strict
UniformSpace st the
carrier of US
= X & the
entourages of US
=
<.(
basis_Pervin_uniformity SF).]
proof
(
basis_Pervin_uniformity SF) is
quasi_basis & (
basis_Pervin_uniformity SF) is
axiom_UP1 & (
basis_Pervin_uniformity SF) is
axiom_UP2 & (
basis_Pervin_uniformity SF) is
axiom_UP3 by
Th37,
Th38,
Th44,
Th43;
hence thesis by
Th7;
end;
definition
let X be
set, SF be
Subset-Family of X;
::
UNIFORM3:def31
func
Pervin_uniform_space SF ->
strict
UniformSpace equals
UniformSpaceStr (# X,
<.(
basis_Pervin_uniformity SF).] #);
coherence
proof
ex US be
strict
UniformSpace st the
carrier of US
= X & the
entourages of US
=
<.(
basis_Pervin_uniformity SF).] by
Th45;
hence thesis;
end;
end