uniform2.miz
begin
reserve X for
set,
A for
Subset of X,
R,S for
Relation of X;
theorem ::
UNIFORM2:1
Th2: (
[:(X
\ A), X:]
\/
[:X, A:])
c=
[:X, X:]
proof
[:X, A:]
c=
[:X, X:] &
[:(X
\ A), X:]
c=
[:X, X:] by
ZFMISC_1: 95;
hence thesis by
XBOOLE_1: 8;
end;
theorem ::
UNIFORM2:2
(
[:(X
\ A), X:]
\/
[:X, A:])
= (
[:A, A:]
\/
[:(X
\ A), X:])
proof
A1: (
[:(X
\ A), X:]
\/
[:X, A:])
c= (
[:A, A:]
\/
[:(X
\ A), X:])
proof
let x be
object;
assume
A2: x
in (
[:(X
\ A), X:]
\/
[:X, A:]);
(
[:(X
\ A), X:]
\/
[:X, A:])
c=
[:X, X:] by
Th2;
then
consider a,b be
object such that
A3: a
in X and
A4: b
in X and
A5: x
=
[a, b] by
A2,
ZFMISC_1:def 2;
per cases ;
suppose
A6: a
in A;
x
in
[:X, A:]
proof
assume not x
in
[:X, A:];
then x
in
[:(X
\ A), X:] by
A2,
XBOOLE_0:def 3;
then a
in (X
\ A) & b
in X by
A5,
ZFMISC_1: 87;
hence contradiction by
A6,
XBOOLE_0:def 5;
end;
then b
in A by
A5,
ZFMISC_1: 87;
then
A7: x
in
[:A, A:] by
A6,
A5,
ZFMISC_1: 87;
[:A, A:]
c= (
[:A, A:]
\/
[:(X
\ A), X:]) by
XBOOLE_1: 7;
hence thesis by
A7;
end;
suppose not a
in A;
then a
in (X
\ A) by
A3,
XBOOLE_0:def 5;
then
A8: x
in
[:(X
\ A), X:] by
A4,
A5,
ZFMISC_1: 87;
[:(X
\ A), X:]
c= (
[:(X
\ A), X:]
\/
[:A, A:]) by
XBOOLE_1: 7;
hence thesis by
A8;
end;
end;
[:A, A:]
c=
[:X, A:] by
ZFMISC_1: 95;
hence thesis by
A1,
XBOOLE_1: 13;
end;
theorem ::
UNIFORM2:3
Th3: (R
* S)
= {
[x, y] where x,y be
Element of X : ex z be
Element of X st
[x, z]
in R &
[z, y]
in S }
proof
reconsider RS = (R
* S) as
Relation of X;
A1: (R
* S)
c= {
[x, y] where x,y be
Element of X : ex z be
Element of X st
[x, z]
in R &
[z, y]
in S }
proof
let t be
object;
assume
A1: t
in (R
* S);
consider x1,x2 be
object such that x1
in X and
A2: x2
in X and
A3: t
=
[x1, x2] by
A1,
ZFMISC_1:def 2;
consider z be
object such that
A4:
[x1, z]
in R and
A5:
[z, x2]
in S by
A1,
A3,
RELAT_1:def 8;
reconsider x1, x2, z1 = z as
Element of X by
A2,
A4,
ZFMISC_1: 87;
[x1, z1]
in R &
[z1, x2]
in S by
A4,
A5;
hence thesis by
A3;
end;
{
[x, y] where x,y be
Element of X : ex z be
Element of X st
[x, z]
in R &
[z, y]
in S }
c= (R
* S)
proof
let t be
object;
assume t
in {
[x, y] where x,y be
Element of X : ex z be
Element of X st
[x, z]
in R &
[z, y]
in S };
then ex x,y be
Element of X st t
=
[x, y] & ex z be
Element of X st
[x, z]
in R &
[z, y]
in S;
hence thesis by
RELAT_1:def 8;
end;
hence thesis by
A1;
end;
registration
let X be
set, cB be
Subset-Family of X;
cluster
<.cB.] -> non
empty;
coherence
proof
per cases ;
suppose cB is
empty;
hence thesis by
CARDFIL2: 15;
end;
suppose
A1: cB is non
empty;
cB
c=
<.cB.] by
CARDFIL2: 18;
hence thesis by
A1;
end;
end;
end
registration
let X be
set, cB be
Subset-Family of
[:X, X:];
cluster ->
Relation-like for
Element of cB;
coherence
proof
let e be
Element of cB;
per cases ;
suppose cB is non
empty;
then e
in cB;
hence thesis;
end;
suppose cB is
empty;
hence thesis by
SUBSET_1:def 1;
end;
end;
end
notation
let X be
set, cB be
Subset-Family of
[:X, X:], B be
Element of cB;
synonym B
[~] for B
~ ;
end
definition
let X be
set, cB be
Subset-Family of
[:X, X:], B be
Element of cB;
:: original:
[~]
redefine
func B
[~] ->
Subset of
[:X, X:] ;
coherence
proof
per cases ;
suppose
A3: cB is non
empty;
(B
~ )
c=
[:X, X:]
proof
let x be
object;
assume
A0: x
in (B
~ );
then
consider a,b be
object such that
A1: x
=
[a, b] by
RELAT_1:def 1;
A2:
[b, a]
in B by
A0,
A1,
RELAT_1:def 7;
B
in cB by
A3;
then b
in X & a
in X by
A2,
ZFMISC_1: 87;
hence thesis by
A1,
ZFMISC_1: 87;
end;
hence thesis;
end;
suppose cB is
empty;
then B
=
{} by
SUBSET_1:def 1;
then (B
~ )
=
{} ;
hence thesis by
XBOOLE_1: 2;
end;
end;
end
notation
let X be
set, cB be
Subset-Family of
[:X, X:];
let B1,B2 be
Element of cB;
synonym B1
[*] B2 for B1
* B2;
end
definition
let X be
set, cB be
Subset-Family of
[:X, X:];
let B1,B2 be
Element of cB;
:: original:
[*]
redefine
func B1
[*] B2 ->
Subset of
[:X, X:] ;
coherence
proof
per cases ;
suppose
A3: cB is non
empty;
(B1
* B2)
c=
[:X, X:]
proof
let x be
object;
assume
A0: x
in (B1
* B2);
then
consider a,b be
object such that
A1: x
=
[a, b] by
RELAT_1:def 1;
consider c be
object such that
A2:
[a, c]
in B1 &
[c, b]
in B2 by
A0,
A1,
RELAT_1:def 8;
B1
in cB & B2
in cB by
A3;
then b
in X & a
in X by
A2,
ZFMISC_1: 87;
hence thesis by
A1,
ZFMISC_1: 87;
end;
hence thesis;
end;
suppose cB is
empty;
then B1
=
{} & B2
=
{} by
SUBSET_1:def 1;
then (B1
* B2)
=
{} ;
hence thesis by
XBOOLE_1: 2;
end;
end;
end
theorem ::
UNIFORM2:4
for X be
set, G be
Subset-Family of X st G is
upper holds (
FinMeetCl G) is
upper
proof
let X be
set, G be
Subset-Family of X;
assume
A1: G is
upper;
now
let Y1,Y2 be
Subset of X;
assume that
A2: Y1
in (
FinMeetCl G) and
A3: Y1
c= Y2;
consider Z be
Subset-Family of X such that
A4: Z
c= G and
A5: Z is
finite and
A6: Y1
= (
Intersect Z) by
A2,
CANTOR_1:def 3;
per cases ;
suppose
A7: Z is
empty;
then Y2
= X by
A6,
A3,
SETFAM_1:def 9;
hence Y2
in (
FinMeetCl G) by
A7,
A6,
SETFAM_1:def 9,
A2;
end;
suppose
A8: Z is non
empty;
set Z2 = the set of all (z
\/ Y2) where z be
Element of Z;
set a = the
Element of Z;
A9: (a
\/ Y2)
in Z2;
Z2
c= (
bool X)
proof
let t be
object;
assume t
in Z2;
then
consider u be
Element of Z such that
A10: t
= (u
\/ Y2);
A11: u
in Z by
A8;
(u
\/ Y2)
c= X by
XBOOLE_1: 8,
A11;
hence thesis by
A10;
end;
then
reconsider Z2 as
Subset-Family of X;
now
now
let x be
object;
assume
A12: x
in Z2;
then
reconsider y = x as
Subset of X;
consider u be
Element of Z such that
A13: y
= (u
\/ Y2) by
A12;
u
in G by
A8,
A4;
hence x
in G by
A13,
XBOOLE_1: 7,
A1;
end;
hence Z2
c= G;
A14: Z is
finite by
A5;
deffunc
F(
Element of Z) = ($1
\/ Y2);
A15: {
F(z) where z be
Element of Z : z
in Z } is
finite from
FRAENKEL:sch 21(
A14);
now
thus {
F(z) where z be
Element of Z : z
in Z }
c= Z2
proof
let x be
object;
assume x
in {
F(z) where z be
Element of Z : z
in Z };
then ex z be
Element of Z st x
=
F(z) & z
in Z;
hence thesis;
end;
thus Z2
c= {
F(z) where z be
Element of Z : z
in Z }
proof
let x be
object;
assume x
in Z2;
then ex z be
Element of Z st x
= (z
\/ Y2);
hence thesis by
A8;
end;
end;
hence Z2 is
finite by
A15;
now
thus Y2
c= (
meet Z2)
proof
let x be
object;
assume
A16: x
in Y2;
now
let YY be
set;
assume
A17: YY
in Z2;
then
reconsider ZZ = YY as
Subset of X;
consider u be
Element of Z such that
A18: ZZ
= (u
\/ Y2) by
A17;
Y2
c= (u
\/ Y2) by
XBOOLE_1: 7;
hence x
in YY by
A16,
A18;
end;
hence thesis by
A9,
SETFAM_1:def 1;
end;
thus (
meet Z2)
c= Y2
proof
let x be
object;
assume
A19: x
in (
meet Z2);
A20: for z be
Element of Z holds x
in (z
\/ Y2)
proof
let z be
Element of Z;
(z
\/ Y2)
in Z2;
hence thesis by
A19,
SETFAM_1:def 1;
end;
for z be
Element of Z holds (x
in z or x
in Y2)
proof
let z be
Element of Z;
x
in (z
\/ Y2) by
A20;
hence thesis by
XBOOLE_0:def 3;
end;
then (for z be
set st z
in Z holds x
in z) or x
in Y2;
then (x
in (
meet Z)) or x
in Y2 by
A8,
SETFAM_1:def 1;
then x
in ((
meet Z)
\/ Y2) by
XBOOLE_0:def 3;
then
A21: x
in (Y1
\/ Y2) by
A8,
A6,
SETFAM_1:def 9;
(Y1
\/ Y2)
c= Y2 by
A3,
XBOOLE_1: 8;
hence thesis by
A21;
end;
end;
hence Y2
= (
Intersect Z2) by
A9,
SETFAM_1:def 9;
end;
hence Y2
in (
FinMeetCl G) by
CANTOR_1:def 3;
end;
end;
hence thesis;
end;
theorem ::
UNIFORM2:5
Th4: R
is_symmetric_in X implies (R
~ )
is_symmetric_in X
proof
assume
A1: R
is_symmetric_in X;
now
let x,y be
object;
assume that
A2: x
in X and
A3: y
in X and
A4:
[x, y]
in (R
~ );
[y, x]
in R by
A4,
RELAT_1:def 7;
then
[x, y]
in R by
A2,
A3,
A1,
RELAT_2:def 3;
hence
[y, x]
in (R
~ ) by
RELAT_1:def 7;
end;
hence thesis by
RELAT_2:def 3;
end;
begin
definition
struct (
1-sorted)
UniformSpaceStr
(# the
carrier ->
set,
the
entourages ->
Subset-Family of
[: the carrier, the carrier:] #)
attr strict
strict;
end
definition
let U be
UniformSpaceStr;
::
UNIFORM2:def1
attr U is
void means the
entourages of U is
empty;
end
definition
let X be
set;
::
UNIFORM2:def2
func
Uniform_Space (X) ->
strict
UniformSpaceStr equals
UniformSpaceStr (# X, (
{} (
bool
[:X, X:])) #);
coherence ;
end
definition
::
UNIFORM2:def3
func
TrivialUniformSpace ->
strict
UniformSpaceStr equals
UniformSpaceStr (#
{} , (
cobool
[:
{} ,
{} :]) #);
coherence ;
::
UNIFORM2:def4
func
NonEmptyTrivialUniformSpace ->
strict
UniformSpaceStr means
:
D1: ex SF be
Subset-Family of
[:
{
{} },
{
{} }:] st SF
=
{
[:
{
{} },
{
{} }:]} & it
=
UniformSpaceStr (#
{
{} }, SF #);
existence
proof
set X =
{
{} };
reconsider SF =
{
[:X, X:]} as
Subset-Family of
[:X, X:] by
ZFMISC_1: 68;
take
UniformSpaceStr (# X, SF #);
thus thesis;
end;
uniqueness ;
end
registration
let X be
empty
set;
cluster (
Uniform_Space X) ->
empty;
coherence ;
end
registration
let X be non
empty
set;
cluster (
Uniform_Space X) -> non
empty;
coherence ;
end
registration
let X be
set;
cluster (
Uniform_Space X) ->
void;
coherence ;
end
registration
cluster
TrivialUniformSpace ->
empty non
void;
coherence ;
cluster
NonEmptyTrivialUniformSpace -> non
empty non
void;
coherence
proof
ex SF be
Subset-Family of
[:
{
{} },
{
{} }:] st SF
=
{
[:
{
{} },
{
{} }:]} &
NonEmptyTrivialUniformSpace
=
UniformSpaceStr (#
{
{} }, SF #) by
D1;
hence thesis;
end;
end
registration
cluster
empty
strict
void for
UniformSpaceStr;
existence
proof
take (
Uniform_Space
{} );
thus thesis;
end;
cluster
empty
strict non
void for
UniformSpaceStr;
existence
proof
take
TrivialUniformSpace ;
thus thesis;
end;
cluster non
empty
strict
void for
UniformSpaceStr;
existence
proof
take (
Uniform_Space
{
{} });
thus thesis;
end;
cluster non
empty
strict non
void for
UniformSpaceStr;
existence
proof
take
NonEmptyTrivialUniformSpace ;
thus thesis;
end;
end
definition
let X be
set, SF be
Subset-Family of
[:X, X:];
::
UNIFORM2:def5
func SF
[~] ->
Subset-Family of
[:X, X:] equals the set of all (S
[~] ) where S be
Element of SF;
coherence
proof
the set of all (S
[~] ) where S be
Element of SF
c= (
bool
[:X, X:])
proof
let x be
object;
assume x
in the set of all (S
[~] ) where S be
Element of SF;
then ex S be
Element of SF st x
= (S
[~] );
hence thesis;
end;
hence thesis;
end;
end
definition
let US be
UniformSpaceStr;
::
UNIFORM2:def6
func US
[~] ->
UniformSpaceStr equals
UniformSpaceStr (# the
carrier of US, (the
entourages of US
[~] ) #);
coherence ;
end
registration
let USS be non
empty
UniformSpaceStr;
cluster (USS
[~] ) -> non
empty;
coherence ;
end
begin
definition
let US be
UniformSpaceStr;
::
UNIFORM2:def7
attr US is
upper means the
entourages of US is
upper;
::
UNIFORM2:def8
attr US is
cap-closed means the
entourages of US is
cap-closed;
::
UNIFORM2:def9
attr US is
axiom_U1 means for S be
Element of the
entourages of US holds (
id the
carrier of US)
c= S;
::
UNIFORM2:def10
attr US is
axiom_U2 means for S be
Element of the
entourages of US holds (S
[~] )
in the
entourages of US;
::
UNIFORM2:def11
attr US is
axiom_U3 means for S be
Element of the
entourages of US holds ex W be
Element of the
entourages of US st (W
[*] W)
c= S;
end
theorem ::
UNIFORM2:6
Th7: for US be non
void
UniformSpaceStr holds US is
axiom_U1 iff for S be
Element of the
entourages of US holds ex R be
Relation of the
carrier of US st R
= S & R
is_reflexive_in the
carrier of US
proof
let US be non
void
UniformSpaceStr;
US is non
void;
then
reconsider SFX = the
entourages of US as non
empty
Subset-Family of
[:the
carrier of US, the
carrier of US:];
hereby
assume
A1: US is
axiom_U1;
now
let S be
Element of the
entourages of US;
S is
Element of SFX;
then
consider R be
Relation of the
carrier of US such that
A2: R
= S;
take R;
thus R
= S by
A2;
now
let x be
object;
assume x
in the
carrier of US;
then
A3:
[x, x]
in (
id the
carrier of US) by
RELAT_1:def 10;
(
id the
carrier of US)
c= S by
A1;
hence
[x, x]
in R by
A3,
A2;
end;
hence R
is_reflexive_in the
carrier of US by
RELAT_2:def 1;
end;
hence for S be
Element of the
entourages of US holds ex R be
Relation of the
carrier of US st (R
= S & R
is_reflexive_in the
carrier of US);
end;
assume
A4: for S be
Element of the
entourages of US holds ex R be
Relation of the
carrier of US st (R
= S & R
is_reflexive_in the
carrier of US);
now
let S be
Element of the
entourages of US;
consider R be
Relation of the
carrier of US such that
A5: R
= S and
A6: R
is_reflexive_in the
carrier of US by
A4;
for x be
object st x
in the
carrier of US holds
[x, x]
in R by
A6,
RELAT_2:def 1;
hence (
id the
carrier of US)
c= S by
A5,
RELAT_1: 47;
end;
hence US is
axiom_U1;
end;
theorem ::
UNIFORM2:7
Th8: for US be non
void
UniformSpaceStr holds US is
axiom_U1 iff for S be
Element of the
entourages of US holds ex R be
total
reflexive
Relation of the
carrier of US st R
= S
proof
let US be non
void
UniformSpaceStr;
US is non
void;
then
reconsider SFX = the
entourages of US as non
empty
Subset-Family of
[:the
carrier of US, the
carrier of US:];
hereby
assume
A2: US is
axiom_U1;
hereby
let S be
Element of the
entourages of US;
consider R be
Relation of the
carrier of US such that
A3: R
= S and
A4: R
is_reflexive_in the
carrier of US by
A2,
Th7;
A5: (
field R)
= the
carrier of US by
A4,
PARTIT_2: 9;
reconsider R as
total
reflexive
Relation of the
carrier of US by
A5,
A4,
TAXONOM1: 3,
PARTFUN1:def 2,
RELAT_2:def 9;
take R;
thus R
= S by
A3;
end;
end;
assume
A6: for S be
Element of the
entourages of US holds ex R be
total
reflexive
Relation of the
carrier of US st R
= S;
now
let S be
Element of the
entourages of US;
consider R be
total
reflexive
Relation of the
carrier of US such that
A7: R
= S by
A6;
reconsider R as
Relation of the
carrier of US;
take R;
thus R
= S by
A7;
now
let x be
object;
assume
A8: x
in the
carrier of US;
(
field R)
= the
carrier of US by
ORDERS_1: 12;
hence
[x, x]
in R by
A8,
RELAT_2:def 9,
RELAT_2:def 1;
end;
hence R
is_reflexive_in the
carrier of US by
RELAT_2:def 1;
end;
hence US is
axiom_U1 by
Th7;
end;
registration
cluster
void -> non
axiom_U2 for
UniformSpaceStr;
coherence ;
end
theorem ::
UNIFORM2:8
for US be
UniformSpaceStr st US is
axiom_U2 holds for S be
Element of the
entourages of US holds (for x,y be
Element of US st
[x, y]
in S holds
[y, x]
in (
union the
entourages of US))
proof
let US be
UniformSpaceStr;
assume
A1: US is
axiom_U2;
let S be
Element of the
entourages of US;
let x,y be
Element of US;
assume
A3:
[x, y]
in S;
reconsider SFX = the
entourages of US as non
empty
Subset-Family of
[:the
carrier of US, the
carrier of US:] by
A1;
A6:
[y, x]
in (S
~ ) by
A3,
RELAT_1:def 7;
(S
~ )
in the
entourages of US by
A1;
hence thesis by
A6,
TARSKI:def 4;
end;
theorem ::
UNIFORM2:9
Th9: for US be non
void
UniformSpaceStr st for S be
Element of the
entourages of US holds ex R be
Relation of the
carrier of US st S
= R & R
is_symmetric_in the
carrier of US holds US is
axiom_U2
proof
let US be non
void
UniformSpaceStr;
assume
A2: for S be
Element of the
entourages of US holds ex R be
Relation of the
carrier of US st S
= R & R
is_symmetric_in the
carrier of US;
A1: US is non
void;
US is
axiom_U2
proof
let S be
Element of the
entourages of US;
consider R be
Relation of the
carrier of US such that
A3: S
= R and
A4: R
is_symmetric_in the
carrier of US by
A2;
thus (S
~ )
in the
entourages of US
proof
(R
~ )
= R
proof
thus (R
~ )
c= R
proof
let x be
object;
assume
A7: x
in (R
~ );
then
consider a,b be
object such that
A8: a
in the
carrier of US and
A9: b
in the
carrier of US and
A10: x
=
[a, b] by
ZFMISC_1:def 2;
[b, a]
in R by
A7,
A10,
RELAT_1:def 7;
hence thesis by
A10,
A4,
A8,
A9,
RELAT_2:def 3;
end;
let x be
object;
assume
A11: x
in R;
then
consider a,b be
object such that
A12: a
in the
carrier of US and
A13: b
in the
carrier of US and
A14: x
=
[a, b] by
ZFMISC_1:def 2;
[b, a]
in (R
~ ) by
A11,
A14,
RELAT_1:def 7;
hence thesis by
Th4,
A4,
A12,
A13,
A14,
RELAT_2:def 3;
end;
hence thesis by
A1,
A3;
end;
end;
hence thesis;
end;
theorem ::
UNIFORM2:10
Th10: for US be non
void
UniformSpaceStr st for S be
Element of the
entourages of US holds ex R be
Relation of the
carrier of US st S
= R & R is
symmetric holds US is
axiom_U2
proof
let US be non
void
UniformSpaceStr;
assume
A2: for S be
Element of the
entourages of US holds ex R be
Relation of the
carrier of US st S
= R & R is
symmetric;
now
let S be
Element of the
entourages of US;
consider R be
Relation of the
carrier of US such that
B1: S
= R and
B2: R is
symmetric by
A2;
take R;
thus S
= R by
B1;
for x,y be
object st x
in the
carrier of US & y
in the
carrier of US &
[x, y]
in R holds
[y, x]
in R by
B2,
PREFER_1: 20;
hence R
is_symmetric_in the
carrier of US by
RELAT_2:def 3;
end;
hence thesis by
Th9;
end;
theorem ::
UNIFORM2:11
for US be non
void
UniformSpaceStr st for S be
Element of the
entourages of US holds ex R be
Tolerance of the
carrier of US st S
= R holds US is
axiom_U1 & US is
axiom_U2
proof
let US be non
void
UniformSpaceStr;
assume
A2: for S be
Element of the
entourages of US holds ex R be
Tolerance of the
carrier of US st S
= R;
for S be
Element of the
entourages of US holds ex R be
total
reflexive
Relation of the
carrier of US st R
= S
proof
let S be
Element of the
entourages of US;
ex R be
Tolerance of the
carrier of US st R
= S by
A2;
hence thesis;
end;
hence US is
axiom_U1 by
Th8;
for S be
Element of the
entourages of US holds ex R be
Relation of the
carrier of US st S
= R & R is
symmetric
proof
let S be
Element of the
entourages of US;
ex R be
Tolerance of the
carrier of US st S
= R by
A2;
hence thesis;
end;
hence US is
axiom_U2 by
Th10;
end;
registration
let X be
empty
set;
cluster (
Uniform_Space X) ->
upper
cap-closed
axiom_U1 non
axiom_U2
axiom_U3;
coherence
proof
set US = (
Uniform_Space X);
set E = the
entourages of US;
thus E is
upper;
thus E is
cap-closed
proof
let Y1,Y2 be
Subset of
[:the
carrier of US, the
carrier of US:];
thus thesis;
end;
thus for S be
Element of E holds (
id the
carrier of US)
c= S;
thus US is non
axiom_U2;
let S be
Element of E;
(S
[*] S)
c= S;
hence thesis;
end;
end
registration
cluster (
Uniform_Space
{
{} }) ->
upper
cap-closed non
axiom_U2;
coherence
proof
set US = (
Uniform_Space
{
{} });
set E = the
entourages of US;
thus E is
upper;
thus E is
cap-closed
proof
let Y1,Y2 be
Subset of
[:the
carrier of US, the
carrier of US:];
thus thesis;
end;
thus US is non
axiom_U2;
end;
cluster
TrivialUniformSpace ->
upper
cap-closed
axiom_U1
axiom_U2
axiom_U3;
coherence
proof
set US =
TrivialUniformSpace ;
set E = the
entourages of US;
A1: E
=
{
{} } by
ENUMSET1: 29;
E is
upper;
hence US is
upper;
for X,Y be
set st X
in E & Y
in E holds (X
/\ Y)
in E;
hence US is
cap-closed by
FINSUB_1:def 2;
for S be
Element of E holds (
id the
carrier of US)
c= S;
hence US is
axiom_U1;
now
let S be
Element of E;
S
in
{
{} } by
A1;
hence (S
~ )
in E by
A1;
end;
hence US is
axiom_U2;
let S be
Element of the
entourages of US;
(S
[*] S)
c= S;
hence thesis;
end;
cluster
NonEmptyTrivialUniformSpace ->
upper
cap-closed
axiom_U1
axiom_U2
axiom_U3;
coherence
proof
set X =
{
{} };
set US =
NonEmptyTrivialUniformSpace ;
set E = the
entourages of US;
consider SF be
Subset-Family of
[:X, X:] such that
B1: SF
=
{
[:X, X:]} and
B2: US
=
UniformSpaceStr (# X, SF #) by
D1;
for Y1,Y2 be
Subset of
[:the
carrier of US, the
carrier of US:] st Y1
in E & Y1
c= Y2 holds Y2
in E
proof
let Y1,Y2 be
Subset of
[:the
carrier of US, the
carrier of US:];
assume that
A2: Y1
in E and
A3: Y1
c= Y2;
A4: Y1
=
[:X, X:] by
B1,
B2,
A2,
TARSKI:def 1;
Y1
= Y2 by
B2,
A3,
A4;
hence thesis by
A2;
end;
hence E is
upper;
for a,b be
Subset of
[:the
carrier of US, the
carrier of US:] st a
in E & b
in E holds (a
/\ b)
in E
proof
let a,b be
Subset of
[:the
carrier of US, the
carrier of US:];
assume that
A5: a
in E and
A6: b
in E;
a
=
[:X, X:] & b
=
[:X, X:] by
B1,
B2,
A5,
A6,
TARSKI:def 1;
hence (a
/\ b)
in E by
B1,
B2,
TARSKI:def 1;
end;
hence US is
cap-closed by
ROUGHS_4:def 2;
for S be
Element of E holds (
id X)
c= S
proof
let S be
Element of E;
S
=
[:X, X:] by
B1,
B2,
TARSKI:def 1;
hence thesis;
end;
hence US is
axiom_U1 by
B2;
thus for S be
Element of E holds (S
~ )
in E
proof
let S be
Element of E;
S
=
[:X, X:] by
B1,
B2,
TARSKI:def 1;
then (S
~ )
=
[:X, X:] by
SYSREL: 5;
hence thesis by
B1,
B2,
TARSKI:def 1;
end;
let S be
Element of E;
take S;
S
=
[:X, X:] by
B1,
B2,
TARSKI:def 1;
hence thesis by
B2;
end;
end
registration
cluster
strict
empty non
void
upper
cap-closed
axiom_U1
axiom_U2
axiom_U3 for
UniformSpaceStr;
existence
proof
take
TrivialUniformSpace ;
thus thesis;
end;
end
registration
cluster
empty ->
axiom_U1 for
strict
UniformSpaceStr;
coherence
proof
let US be
strict
UniformSpaceStr;
assume US is
empty;
hence for S be
Element of the
entourages of US holds (
id the
carrier of US)
c= S;
end;
end
registration
cluster
strict non
empty non
void
upper
cap-closed
axiom_U1
axiom_U2
axiom_U3 for
UniformSpaceStr;
existence
proof
take
NonEmptyTrivialUniformSpace ;
thus thesis;
end;
end
definition
let SUS be non
empty
axiom_U1
UniformSpaceStr, x be
Element of SUS, V be
Element of the
entourages of SUS;
::
UNIFORM2:def12
func
Neighborhood (V,x) -> non
empty
Subset of SUS equals { y where y be
Element of SUS :
[x, y]
in V };
coherence
proof
A1: { y where y be
Element of SUS :
[x, y]
in V }
c= the
carrier of SUS
proof
let z be
object;
assume z
in { y where y be
Element of SUS :
[x, y]
in V };
then ex y be
Element of SUS st z
= y &
[x, y]
in V;
hence thesis;
end;
SUS is
axiom_U1;
then
A2: (
id the
carrier of SUS)
c= V;
[x, x]
in (
id the
carrier of SUS) by
RELAT_1:def 10;
then x
in { y where y be
Element of SUS :
[x, y]
in V } by
A2;
hence thesis by
A1;
end;
end
theorem ::
UNIFORM2:12
for USS be non
empty
axiom_U1
UniformSpaceStr, x be
Element of the
carrier of USS, V be
Element of the
entourages of USS holds x
in (
Neighborhood (V,x))
proof
let USS be non
empty
axiom_U1
UniformSpaceStr, x be
Element of USS, V be
Element of the
entourages of USS;
USS is
axiom_U1;
then
A1: (
id the
carrier of USS)
c= V;
[x, x]
in (
id the
carrier of USS) by
RELAT_1:def 10;
hence thesis by
A1;
end;
definition
let USS be
cap-closed
UniformSpaceStr, V1,V2 be
Element of the
entourages of USS;
:: original:
/\
redefine
func V1
/\ V2 ->
Element of the
entourages of USS ;
coherence
proof
per cases ;
suppose the
entourages of USS is
empty;
then V1
=
{} & V2
=
{} by
SUBSET_1:def 1;
hence thesis;
end;
suppose
A1: the
entourages of USS is non
empty;
USS is
cap-closed;
hence thesis by
A1,
FINSUB_1:def 2;
end;
end;
end
theorem ::
UNIFORM2:13
Th11: for USS be non
empty
cap-closed
axiom_U1
UniformSpaceStr, x be
Element of USS, V,W be
Element of the
entourages of USS holds ((
Neighborhood (V,x))
/\ (
Neighborhood (W,x)))
= (
Neighborhood ((V
/\ W),x))
proof
let USS be non
empty
cap-closed
axiom_U1
UniformSpaceStr, x be
Element of USS, V,W be
Element of the
entourages of USS;
set NV = (
Neighborhood (V,x)), NW = (
Neighborhood (W,x)), NVW = (
Neighborhood ((V
/\ W),x));
A1: (NV
/\ NW)
c= NVW
proof
let t be
object;
assume
A2: t
in (NV
/\ NW);
then t
in { y where y be
Element of USS :
[x, y]
in V } by
XBOOLE_0:def 4;
then
consider y1 be
Element of USS such that
A3: t
= y1 and
A4:
[x, y1]
in V;
t
in { y where y be
Element of USS :
[x, y]
in W } by
A2,
XBOOLE_0:def 4;
then
consider y2 be
Element of USS such that
A5: t
= y2 and
A6:
[x, y2]
in W;
[x, y1]
in (V
/\ W) &
[x, y2]
in (V
/\ W) by
A3,
A4,
A5,
A6,
XBOOLE_0:def 4;
hence thesis by
A3;
end;
NVW
c= (NV
/\ NW)
proof
let t be
object;
assume t
in NVW;
then
consider y be
Element of USS such that
A7: t
= y and
A8:
[x, y]
in (V
/\ W);
A9:
[x, y]
in V &
[x, y]
in W by
A8,
XBOOLE_0:def 4;
then
A10: t
in NV by
A7;
t
in { y where y be
Element of USS :
[x, y]
in W } by
A7,
A9;
hence t
in (NV
/\ NW) by
A10,
XBOOLE_0:def 4;
end;
hence thesis by
A1;
end;
registration
let USS be non
empty
axiom_U1
UniformSpaceStr;
cluster the
entourages of USS ->
with_non-empty_elements;
coherence
proof
assume not the
entourages of USS is
with_non-empty_elements;
then
A1:
{}
in the
entourages of USS by
SETFAM_1:def 8;
USS is
axiom_U1;
then (
id the
carrier of USS)
c=
{} by
A1;
hence thesis;
end;
end
registration
let USS be non
empty
axiom_U1
UniformSpaceStr;
cluster the
entourages of USS -> non
empty;
coherence
proof
assume the
entourages of USS is
empty;
then
reconsider S =
{} as
Element of the
entourages of USS by
SUBSET_1:def 1;
USS is
axiom_U1;
then (
id the
carrier of USS)
c= S;
hence thesis;
end;
end
definition
let USS be non
empty
axiom_U1
UniformSpaceStr, x be
Point of USS;
::
UNIFORM2:def13
func
Neighborhood (x) ->
Subset-Family of USS equals the set of all (
Neighborhood (V,x)) where V be
Element of the
entourages of USS;
coherence
proof
set SN = the set of all (
Neighborhood (V,x)) where V be
Element of the
entourages of USS;
SN
c= (
bool the
carrier of USS)
proof
let t be
object;
assume t
in SN;
then ex V be
Element of the
entourages of USS st t
= (
Neighborhood (V,x));
hence thesis;
end;
hence thesis;
end;
end
registration
let USS be non
empty
axiom_U1
UniformSpaceStr, x be
Point of USS;
cluster (
Neighborhood x) -> non
empty;
coherence
proof
set SN = (
Neighborhood x);
the
entourages of USS is non
empty;
then
consider V0 be
object such that
A2: V0
in the
entourages of USS;
reconsider V1 = V0 as
Element of the
entourages of USS by
A2;
(
Neighborhood (V1,x))
in SN;
hence thesis;
end;
end
theorem ::
UNIFORM2:14
for SUS be non
empty
axiom_U1
UniformSpaceStr, x be
Element of the
carrier of SUS, V be
Element of the
entourages of SUS holds (
Neighborhood (V,x))
= (V
.:
{x}) & (
Neighborhood (V,x))
= (
rng (V
|
{x})) & (
Neighborhood (V,x))
= (
Im (V,x)) & (
Neighborhood (V,x))
= (
Class (V,x)) & (
Neighborhood (V,x))
= (
neighbourhood (x,V))
proof
let SUS be non
empty
axiom_U1
UniformSpaceStr, x be
Element of the
carrier of SUS, V be
Element of the
entourages of SUS;
thus (
Neighborhood (V,x))
= (V
.:
{x})
proof
thus (
Neighborhood (V,x))
c= (V
.:
{x})
proof
let t be
object;
assume t
in (
Neighborhood (V,x));
then
consider y be
Element of SUS such that
A3: t
= y and
A4:
[x, y]
in V;
x
in
{x} by
TARSKI:def 1;
hence thesis by
A3,
A4,
RELAT_1:def 13;
end;
let t be
object;
assume t
in (V
.:
{x});
then
consider v be
object such that
A5:
[v, t]
in V and
A6: v
in
{x} by
RELAT_1:def 13;
A7: t
in the
carrier of SUS by
A5,
ZFMISC_1: 87;
[x, t]
in V by
A5,
A6,
TARSKI:def 1;
hence thesis by
A7;
end;
hence thesis by
RELAT_1: 115;
end;
definition
let USS be non
empty
axiom_U1
UniformSpaceStr;
::
UNIFORM2:def14
func
Neighborhood (USS) ->
Function of the
carrier of USS, (
bool (
bool the
carrier of USS)) means
:
Def5: for x be
Element of USS holds (it
. x)
= (
Neighborhood x);
existence
proof
defpred
P[
object,
object] means ex x be
Element of USS st x
= $1 & $2
= (
Neighborhood x);
A1: for x be
object st x
in the
carrier of USS holds ex y be
object st y
in (
bool (
bool the
carrier of USS)) &
P[x, y]
proof
let x be
object;
assume x
in the
carrier of USS;
then
reconsider y = x as
Element of USS;
take z = (
Neighborhood y);
thus z
in (
bool (
bool the
carrier of USS));
thus
P[x, z];
end;
consider f be
Function of the
carrier of USS, (
bool (
bool the
carrier of USS)) such that
A2: for x be
object st x
in the
carrier of USS holds
P[x, (f
. x)] from
FUNCT_2:sch 1(
A1);
take f;
hereby
let x be
Element of USS;
P[x, (f
. x)] by
A2;
hence (f
. x)
= (
Neighborhood x);
end;
end;
uniqueness
proof
let F1,F2 be
Function of the
carrier of USS, (
bool (
bool the
carrier of USS)) such that
A3: for x be
Element of USS holds (F1
. x)
= (
Neighborhood x) and
A4: for x be
Element of USS holds (F2
. x)
= (
Neighborhood x);
now
thus (
dom F1)
= the
carrier of USS by
FUNCT_2:def 1
.= (
dom F2) by
FUNCT_2:def 1;
hereby
let x be
object;
assume x
in (
dom F1);
then
reconsider y = x as
Element of USS;
(F1
. y)
= (
Neighborhood y) by
A3;
hence (F1
. x)
= (F2
. x) by
A4;
end;
end;
hence thesis by
FUNCT_1:def 11;
end;
end
definition
let USS be non
empty
axiom_U1
UniformSpaceStr;
::
UNIFORM2:def15
attr USS is
topological means
FMT_Space_Str (# the
carrier of USS, (
Neighborhood USS) #) is
FMT_TopSpace;
end
begin
definition
mode
Quasi-UniformSpace is
upper
cap-closed
axiom_U1
axiom_U3
UniformSpaceStr;
end
reserve QUS for
Quasi-UniformSpace;
theorem ::
UNIFORM2:15
the
entourages of QUS is
empty implies the
entourages of (QUS
[~] )
=
{
{} }
proof
assume
A1: the
entourages of QUS is
empty;
reconsider EQUS = the
entourages of QUS as
Subset-Family of
[:the
carrier of QUS, the
carrier of QUS:];
set X = the set of all (U
~ ) where U be
Element of the
entourages of QUS;
X
=
{
{} }
proof
thus X
c=
{
{} }
proof
let x be
object;
assume x
in X;
then
consider U be
Element of the
entourages of QUS such that
A11: x
= (U
~ );
U
=
{} by
A1,
SUBSET_1:def 1;
then x
=
{} by
A11;
hence thesis by
TARSKI:def 1;
end;
let x be
object;
assume x
in
{
{} };
then
A14: x
=
{} by
TARSKI:def 1;
then
reconsider y = x as
Element of the
entourages of QUS by
A1,
SUBSET_1:def 1;
(y
~ )
=
{} by
A14;
hence thesis by
A14;
end;
hence thesis;
end;
theorem ::
UNIFORM2:16
the
entourages of (QUS
[~] )
=
{
{} } & the
entourages of (QUS
[~] ) is
upper implies the
carrier of QUS is
empty
proof
assume that
A1: the
entourages of (QUS
[~] )
=
{
{} } and
A2: the
entourages of (QUS
[~] ) is
upper;
reconsider X = the
carrier of QUS as
set;
[:X, X:]
c=
[:the
carrier of (QUS
[~] ), the
carrier of (QUS
[~] ):];
then
reconsider XX =
[:X, X:] as
Subset of
[:the
carrier of (QUS
[~] ), the
carrier of (QUS
[~] ):];
{}
c=
[:the
carrier of (QUS
[~] ), the
carrier of (QUS
[~] ):];
then
reconsider Y =
{} as
Subset of
[:the
carrier of (QUS
[~] ), the
carrier of (QUS
[~] ):];
Y
in the
entourages of (QUS
[~] ) & Y
c= XX by
A1,
TARSKI:def 1;
then XX
in the
entourages of (QUS
[~] ) by
A2;
hence thesis by
A1,
TARSKI:def 1;
end;
registration
let QUS be non
void
Quasi-UniformSpace;
cluster (QUS
[~] ) ->
upper
cap-closed
axiom_U1
axiom_U3;
coherence
proof
A1: QUS is non
void;
reconsider EQUS = the
entourages of QUS as
Subset-Family of
[:the
carrier of QUS, the
carrier of QUS:];
A10: the
entourages of (QUS
[~] ) is non
empty
proof
assume
A11: the
entourages of (QUS
[~] ) is
empty;
set S = the
Element of the
entourages of QUS;
reconsider S as
Element of the
entourages of QUS;
(S
~ )
in (the
entourages of QUS
[~] );
hence contradiction by
A11;
end;
for Y1,Y2 be
Subset of
[:the
carrier of (QUS
[~] ), the
carrier of (QUS
[~] ):] st Y1
in the
entourages of (QUS
[~] ) & Y1
c= Y2 holds Y2
in the
entourages of (QUS
[~] )
proof
let Y1,Y2 be
Subset of
[:the
carrier of (QUS
[~] ), the
carrier of (QUS
[~] ):];
assume that
A12: Y1
in the
entourages of (QUS
[~] ) and
A13: Y1
c= Y2;
consider U1 be
Element of the
entourages of QUS such that
A14: Y1
= (U1
~ ) by
A12;
A15: (Y1
~ )
= U1 by
A14;
QUS is
upper;
then
reconsider U2 = (Y2
~ ) as
Element of the
entourages of QUS by
A13,
SYSREL: 11,
A15,
CARDFIL2:def 1,
A1;
consider R2 be
Relation of the
carrier of QUS such that
A16: Y2
= R2 and (Y2
~ )
= (R2
~ );
(U2
~ )
= ((R2
~ )
~ ) by
A16;
hence thesis;
end;
then the
entourages of (QUS
[~] ) is
upper;
hence (QUS
[~] ) is
upper;
for Y1,Y2 be
set st Y1
in the
entourages of (QUS
[~] ) & Y2
in the
entourages of (QUS
[~] ) holds (Y1
/\ Y2)
in the
entourages of (QUS
[~] )
proof
let Y1,Y2 be
set;
assume that
A17: Y1
in the
entourages of (QUS
[~] ) and
A18: Y2
in the
entourages of (QUS
[~] );
consider U1 be
Element of the
entourages of QUS such that
A19: Y1
= (U1
~ ) by
A17;
consider U2 be
Element of the
entourages of QUS such that
A20: Y2
= (U2
~ ) by
A18;
reconsider U12 = (U1
/\ U2) as
Element of the
entourages of QUS;
(Y1
/\ Y2)
= (U12
~ ) by
A19,
A20,
RELAT_1: 22;
hence thesis;
end;
hence (QUS
[~] ) is
cap-closed by
FINSUB_1:def 2;
thus for S be
Element of the
entourages of (QUS
[~] ) holds (
id the
carrier of (QUS
[~] ))
c= S
proof
let S be
Element of the
entourages of (QUS
[~] );
S
in the set of all (U
~ ) where U be
Element of the
entourages of QUS by
A10;
then
consider U be
Element of the
entourages of QUS such that
A21: S
= (U
~ );
QUS is
axiom_U1;
then ((
id the
carrier of QUS)
~ )
c= (U
~ ) by
SYSREL: 11;
hence thesis by
A21;
end;
thus for S be
Element of the
entourages of (QUS
[~] ) holds ex W be
Element of the
entourages of (QUS
[~] ) st (W
* W)
c= S
proof
let S be
Element of the
entourages of (QUS
[~] );
S
in the
entourages of (QUS
[~] ) by
A10;
then
consider U be
Element of the
entourages of QUS such that
A24: S
= (U
~ );
QUS is
axiom_U3;
then
consider W be
Element of the
entourages of QUS such that
A27: (W
* W)
c= U;
(W
~ )
in (the
entourages of QUS
[~] );
then
reconsider W2 = (W
[~] ) as
Element of the
entourages of (QUS
[~] );
take W2;
let t be
object;
assume
A30: t
in (W2
* W2);
t
in {
[x, y] where x,y be
Element of QUS : ex z be
Element of QUS st
[x, z]
in W2 &
[z, y]
in W2 } by
A30,
Th3;
then
consider x,y be
Element of QUS such that
A34: t
=
[x, y] and
A35: ex z be
Element of QUS st
[x, z]
in W2 &
[z, y]
in W2;
consider z be
Element of QUS such that
A36:
[x, z]
in W2 and
A37:
[z, y]
in W2 by
A35;
A38:
[z, x]
in ((W
~ )
~ ) by
A36,
RELAT_1:def 7;
[y, z]
in ((W
~ )
~ ) by
A37,
RELAT_1:def 7;
then
[y, x]
in (W
* W) by
A38,
RELAT_1:def 8;
hence thesis by
A24,
A34,
A27,
RELAT_1:def 7;
end;
end;
end
definition
let X be
set, cB be
Subset-Family of
[:X, X:];
::
UNIFORM2:def16
attr cB is
axiom_UP1 means for B be
Element of cB holds (
id X)
c= B;
::
UNIFORM2:def17
attr cB is
axiom_UP3 means for B1 be
Element of cB holds ex B2 be
Element of cB st (B2
[*] B2)
c= B1;
end
theorem ::
UNIFORM2:17
for X be non
empty
set, cB be
empty
Subset-Family of
[:X, X:] holds not cB is
axiom_UP1
proof
let X be non
empty
set, cB be
empty
Subset-Family of
[:X, X:];
assume
A1: cB is
axiom_UP1;
{} is
Element of cB by
SUBSET_1:def 1;
then (
id X)
c=
{} by
A1;
hence thesis;
end;
theorem ::
UNIFORM2:18
Th11bis: for X be
set, cB be
Subset-Family of
[:X, X:] st cB is
quasi_basis & cB is
axiom_UP1 & cB is
axiom_UP3 holds
UniformSpaceStr (# X,
<.cB.] #) is
Quasi-UniformSpace
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
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 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;
hence thesis;
end;
begin
definition
mode
Semi-UniformSpace is
upper
cap-closed
axiom_U1
axiom_U2
UniformSpaceStr;
end
reserve SUS for
Semi-UniformSpace;
registration
cluster -> non
void for
Semi-UniformSpace;
coherence ;
end
theorem ::
UNIFORM2:19
Th12: SUS is
empty implies
{}
in the
entourages of SUS
proof
assume
A1: SUS is
empty;
assume
A2: not
{}
in the
entourages of SUS;
SUS is non
void;
then the
entourages of SUS is non
empty;
hence thesis by
A1,
A2;
end;
registration
let SUS be
empty
Semi-UniformSpace;
cluster the
entourages of SUS ->
with_empty_element;
coherence by
Th12,
SETFAM_1:def 8;
end
begin
definition
let SUS be non
empty
Semi-UniformSpace;
::
UNIFORM2:def18
attr SUS is
axiom_UL means for S be
Element of the
entourages of SUS, x be
Element of SUS holds ex W be
Element of the
entourages of SUS st { y where y be
Element of SUS :
[x, y]
in (W
[*] W) }
c= (
Neighborhood (S,x));
end
registration
cluster
axiom_U3 ->
axiom_UL for non
empty
Semi-UniformSpace;
coherence
proof
let US be non
empty
Semi-UniformSpace;
assume
A1: US is
axiom_U3;
let S be
Element of the
entourages of US, x be
Element of US;
consider W be
Element of the
entourages of US such that
A2: (W
* W)
c= S by
A1;
{ y where y be
Element of US :
[x, y]
in (W
* W) }
c= (
Neighborhood (S,x))
proof
let t be
object;
assume t
in { y where y be
Element of US :
[x, y]
in (W
* W) };
then ex y0 be
Element of US st t
= y0 &
[x, y0]
in (W
* W);
hence thesis by
A2;
end;
hence thesis;
end;
end
registration
cluster
axiom_UL for non
empty
Semi-UniformSpace;
existence
proof
take the
axiom_U3 non
empty
Semi-UniformSpace;
thus thesis;
end;
end
definition
mode
Locally-UniformSpace is
axiom_UL non
empty
Semi-UniformSpace;
end
theorem ::
UNIFORM2:20
Th15: for USS be non
empty
upper
axiom_U1
UniformSpaceStr, x be
Element of the
carrier of USS holds (
Neighborhood x) is
upper
proof
let US be non
empty
upper
axiom_U1
UniformSpaceStr, x be
Element of US;
set N = (
Neighborhood x);
now
let S1,S2 be
Subset of US;
assume that
A1: S1
in N and
A2: S1
c= S2;
consider V1 be
Element of the
entourages of US such that
A3: S1
= (
Neighborhood (V1,x)) by
A1;
A4: V1
c= (
[:
{x}, S1:]
\/ (
[:the
carrier of US, the
carrier of US:]
\
[:
{x}, the
carrier of US:]))
proof
let t be
object;
assume
A5: t
in V1;
consider a,b be
object such that a
in the
carrier of US and
A7: b
in the
carrier of US and
A8: t
=
[a, b] by
A5,
ZFMISC_1:def 2;
reconsider b as
Element of US by
A7;
per cases ;
suppose
A9: x
= a;
then x
in
{x} & b
in S1 by
A3,
A5,
A8,
TARSKI:def 1;
then
A10: t
in
[:
{x}, S1:] by
A9,
A8,
ZFMISC_1:def 2;
[:
{x}, S1:]
c= (
[:
{x}, S1:]
\/ (
[:the
carrier of US, the
carrier of US:]
\
[:
{x}, the
carrier of US:])) by
XBOOLE_1: 7;
hence thesis by
A10;
end;
suppose
A11: not x
= a;
A12: not
[a, b]
in
[:
{x}, the
carrier of US:]
proof
assume
[a, b]
in
[:
{x}, the
carrier of US:];
then ex c,d be
object st c
in
{x} & d
in the
carrier of US &
[a, b]
=
[c, d] by
ZFMISC_1:def 2;
then a
in
{x} & b
in the
carrier of US by
XTUPLE_0: 1;
hence thesis by
A11,
TARSKI:def 1;
end;
A13: t
in (
[:the
carrier of US, the
carrier of US:]
\
[:
{x}, the
carrier of US:]) by
A5,
A12,
A8,
XBOOLE_0:def 5;
(
[:the
carrier of US, the
carrier of US:]
\
[:
{x}, the
carrier of US:])
c= (
[:
{x}, S1:]
\/ (
[:the
carrier of US, the
carrier of US:]
\
[:
{x}, the
carrier of US:])) by
XBOOLE_1: 7;
hence thesis by
A13;
end;
end;
reconsider V2 = (
[:
{x}, S2:]
\/ (
[:the
carrier of US, the
carrier of US:]
\
[:
{x}, the
carrier of US:])) as
Subset of
[:the
carrier of US, the
carrier of US:];
A15: V1
c= V2
proof
[:
{x}, S1:]
c=
[:
{x}, S2:] by
A2,
ZFMISC_1: 95;
then (
[:
{x}, S1:]
\/ (
[:the
carrier of US, the
carrier of US:]
\
[:
{x}, the
carrier of US:]))
c= (
[:
{x}, S2:]
\/ (
[:the
carrier of US, the
carrier of US:]
\
[:
{x}, the
carrier of US:])) by
XBOOLE_1: 9;
hence thesis by
A4;
end;
US is
upper;
then the
entourages of US is
upper;
then
reconsider V2 as
Element of the
entourages of US by
A15;
S2
= (
Neighborhood (V2,x))
proof
A16: S2
c= (
Neighborhood (V2,x))
proof
let t be
object;
assume
A17: t
in S2;
then
reconsider t1 = t as
Element of US;
A18: x
in
{x} by
TARSKI:def 1;
[x, t1]
in
[:
{x}, S2:] by
A17,
A18,
ZFMISC_1:def 2;
then
[x, t1]
in V2 by
XBOOLE_0:def 3;
hence thesis;
end;
(
Neighborhood (V2,x))
c= S2
proof
let t be
object;
assume t
in (
Neighborhood (V2,x));
then ex y0 be
Element of US st t
= y0 &
[x, y0]
in V2;
per cases by
XBOOLE_0:def 3;
suppose
[x, t]
in
[:
{x}, S2:];
then ex a,b be
object st a
in
{x} & b
in S2 &
[x, t]
=
[a, b] by
ZFMISC_1:def 2;
hence thesis by
XTUPLE_0: 1;
end;
suppose
A19:
[x, t]
in (
[:the
carrier of US, the
carrier of US:]
\
[:
{x}, the
carrier of US:]);
then ex a,b be
object st a
in the
carrier of US & b
in the
carrier of US &
[x, t]
=
[a, b] by
ZFMISC_1:def 2;
then
A20: t
in the
carrier of US by
XTUPLE_0: 1;
x
in
{x} by
TARSKI:def 1;
then
[x, t]
in
[:
{x}, the
carrier of US:] by
A20,
ZFMISC_1:def 2;
hence thesis by
A19,
XBOOLE_0:def 5;
end;
end;
hence thesis by
A16;
end;
hence S2
in N;
end;
hence thesis;
end;
theorem ::
UNIFORM2:21
Th16: for US be non
empty
axiom_U1
UniformSpaceStr, x be
Element of US, V be
Element of the
entourages of US holds x
in (
Neighborhood (V,x))
proof
let US be non
empty
axiom_U1
UniformSpaceStr, x be
Element of US, V be
Element of the
entourages of US;
US is
axiom_U1;
then
A1: (
id the
carrier of US)
c= V;
[x, x]
in (
id the
carrier of US) by
RELAT_1:def 10;
hence thesis by
A1;
end;
theorem ::
UNIFORM2:22
Th17: for US be non
empty
cap-closed
axiom_U1
UniformSpaceStr, x be
Element of US holds (
Neighborhood x) is
cap-closed
proof
let US be non
empty
cap-closed
axiom_U1
UniformSpaceStr, x be
Element of US;
set N = (
Neighborhood x);
now
let Y1,Y2 be
set;
assume that
A1: Y1
in N and
A2: Y2
in N;
consider V1 be
Element of the
entourages of US such that
A3: Y1
= (
Neighborhood (V1,x)) by
A1;
consider V2 be
Element of the
entourages of US such that
A4: Y2
= (
Neighborhood (V2,x)) by
A2;
(Y1
/\ Y2)
= (
Neighborhood ((V1
/\ V2),x)) by
A3,
A4,
Th11;
hence (Y1
/\ Y2)
in N;
end;
hence thesis by
FINSUB_1:def 2;
end;
theorem ::
UNIFORM2:23
Th18: for US be non
empty
upper
cap-closed
axiom_U1
UniformSpaceStr, x be
Element of US holds (
Neighborhood x) is
Filter of the
carrier of US
proof
let US be non
empty
upper
cap-closed
axiom_U1
UniformSpaceStr, x be
Element of US;
set N = (
Neighborhood x);
now
thus not
{}
in N
proof
assume
{}
in N;
then ex V be
Element of the
entourages of US st
{}
= (
Neighborhood (V,x));
hence thesis;
end;
hereby
let Y1,Y2 be
Subset of US;
hereby
assume that
A1: Y1
in N and
A2: Y2
in N;
N is
cap-closed by
Th17;
hence (Y1
/\ Y2)
in N by
A1,
A2,
FINSUB_1:def 2;
end;
hereby
assume that
A3: Y1
in N and
A4: Y1
c= Y2;
N is
upper by
Th15;
hence Y2
in N by
A3,
A4;
end;
end;
end;
hence thesis by
CARD_FIL:def 1;
end;
registration
cluster ->
topological for
Locally-UniformSpace;
coherence
proof
let LUS be
Locally-UniformSpace;
set UT =
FMT_Space_Str (# the
carrier of LUS, (
Neighborhood LUS) #);
reconsider UT as non
empty
strict
FMT_Space_Str;
A1: for x be
Element of UT holds ex y be
Element of LUS st x
= y & (
U_FMT x)
= (
Neighborhood y)
proof
let x be
Element of UT;
(
U_FMT x)
= (the
BNbd of UT
. x) by
FINTOPO2:def 6;
then
consider y be
Element of LUS such that
A2: x
= y and
A3: (
U_FMT x)
= ((
Neighborhood LUS)
. y);
((
Neighborhood LUS)
. y)
= (
Neighborhood y) by
Def5;
hence thesis by
A2,
A3;
end;
now
for x be
Element of UT, V be
Element of (
U_FMT x) holds ex W be
Element of (
U_FMT x) st for y be
Element of UT st y is
Element of W holds V is
Element of (
U_FMT y)
proof
let x be
Element of UT, V be
Element of (
U_FMT x);
consider y be
Element of LUS such that x
= y and
A4: (
U_FMT x)
= (
Neighborhood y) by
A1;
A5: V
in (
Neighborhood y) by
A4;
then
consider V0 be
Element of the
entourages of LUS such that
A6: V
= (
Neighborhood (V0,y));
LUS is
axiom_UL;
then
consider W be
Element of the
entourages of LUS such that
A7: { z where z be
Element of LUS :
[y, z]
in (W
* W) }
c= (
Neighborhood (V0,y));
(
Neighborhood (W,y))
in the set of all (
Neighborhood (V,y)) where V be
Element of the
entourages of LUS;
then
reconsider WN = (
Neighborhood (W,y)) as
Element of (
Neighborhood y);
A8: for t,z be
object st
[y, t]
in W &
[t, z]
in W holds
[y, z]
in V0
proof
let t,z be
object;
assume that
A9:
[y, t]
in W and
A10:
[t, z]
in W;
consider R1,R2 be
Relation of the
carrier of LUS such that
A11: W
= R1 and
A12: W
= R2 and (W
* W)
= (R1
* R2);
AAA:
[y, z]
in (R1
* R2) by
A9,
A10,
A11,
A12,
RELAT_1:def 8;
consider a,b be
object such that a
in the
carrier of LUS and
A12B: b
in the
carrier of LUS and
A12C:
[t, z]
=
[a, b] by
A10,
ZFMISC_1:def 2;
reconsider z as
Element of LUS by
A12C,
A12B,
XTUPLE_0: 1;
z
in { z where z be
Element of LUS :
[y, z]
in (W
* W) } by
AAA,
A11,
A12;
then z
in (
Neighborhood (V0,y)) by
A7;
then ex z0 be
Element of LUS st z
= z0 &
[y, z0]
in V0;
hence thesis;
end;
reconsider WN as
Element of (
U_FMT x) by
A4;
take WN;
hereby
let z be
Element of UT;
assume z is
Element of WN;
then z
in { z where z be
Element of LUS :
[y, z]
in W };
then
consider z0 be
Element of LUS such that
A13: z
= z0 and
A14:
[y, z0]
in W;
consider z1 be
Element of LUS such that
A15: z
= z1 and
A16: (
U_FMT z)
= (
Neighborhood z1) by
A1;
A17: (
Neighborhood (W,z1))
c= (
Neighborhood (V0,y))
proof
let t be
object;
assume t
in (
Neighborhood (W,z1));
then
consider y0 be
Element of LUS such that
A18: t
= y0 and
A19:
[z1, y0]
in W;
[y, t]
in V0 by
A18,
A19,
A15,
A13,
A14,
A8;
hence thesis by
A18;
end;
(
Neighborhood (W,z1))
in (
Neighborhood z1);
then
reconsider WW = (
Neighborhood (W,z1)) as
Element of (
Neighborhood z1);
reconsider WW2 = WW, V2 = V as
Subset of LUS by
A5;
A20: WW2
c= V2 by
A6,
A17;
(
Neighborhood z1) is
upper by
Th15;
hence V is
Element of (
U_FMT z) by
A16,
A20;
end;
end;
hence UT is
U_FMT_local;
for x be
Element of UT, V be
Element of (
U_FMT x) holds x
in V
proof
let x be
Element of UT, V be
Element of (
U_FMT x);
consider y be
Element of LUS such that
A21: x
= y and
A22: (
U_FMT x)
= (
Neighborhood y) by
A1;
V
in the set of all (
Neighborhood (V,y)) where V be
Element of the
entourages of LUS by
A22;
then ex W be
Element of the
entourages of LUS st V
= (
Neighborhood (W,y));
hence thesis by
A21,
Th16;
end;
hence UT is
U_FMT_with_point;
for x be
Element of UT holds (
U_FMT x) is
Filter of the
carrier of UT
proof
let x be
Element of UT;
ex y be
Element of LUS st x
= y & (
U_FMT x)
= (
Neighborhood y) by
A1;
hence thesis by
Th18;
end;
hence UT is
U_FMT_filter;
end;
hence thesis;
end;
end
begin
definition
let USS be
topological non
empty
axiom_U1
UniformSpaceStr;
::
UNIFORM2:def19
func
FMT_induced_by (USS) -> non
empty
strict
FMT_TopSpace equals
FMT_Space_Str (# the
carrier of USS, (
Neighborhood USS) #);
coherence
proof
USS is
topological;
hence thesis;
end;
end
definition
let USS be
topological non
empty
axiom_U1
UniformSpaceStr;
::
UNIFORM2:def20
func
TopSpace_induced_by (USS) ->
TopSpace equals (
FMT2TopSpace (
FMT_induced_by USS));
coherence ;
end
begin
definition
let X be
set, A be
Subset of X;
::
UNIFORM2:def21
func
block_Pervin_quasi_uniformity (A) ->
Subset of
[:X, X:] equals (
[:(X
\ A), X:]
\/
[:X, A:]);
coherence
proof
A1:
[:(X
\ A), X:]
c=
[:X, X:] by
ZFMISC_1: 95;
[:X, A:]
c=
[:X, X:] by
ZFMISC_1: 95;
hence thesis by
A1,
XBOOLE_1: 8;
end;
end
theorem ::
UNIFORM2:24
Th20: (
id X)
c= (
block_Pervin_quasi_uniformity A) & ((
block_Pervin_quasi_uniformity A)
* (
block_Pervin_quasi_uniformity A))
c= (
block_Pervin_quasi_uniformity A)
proof
thus (
id X)
c= (
block_Pervin_quasi_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
A4:
[a, b]
in
[:A, A:] by
ZFMISC_1:def 2;
A5:
[:A, A:]
c=
[:X, A:] by
ZFMISC_1: 96;
[:X, A:]
c= (
block_Pervin_quasi_uniformity A) by
XBOOLE_1: 7;
hence thesis by
A4,
A2,
A5;
end;
suppose not a
in A;
then a
in (X
\ A) by
A3,
XBOOLE_0:def 5;
then
A6: t
in
[:(X
\ A), X:] by
A2,
A3,
ZFMISC_1:def 2;
[:(X
\ A), X:]
c= (
block_Pervin_quasi_uniformity A) by
XBOOLE_1: 7;
hence thesis by
A6;
end;
end;
now
let t be
object;
assume
A7: t
in ((
block_Pervin_quasi_uniformity A)
* (
block_Pervin_quasi_uniformity A));
then
consider a,b be
object such that
A8: 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_quasi_uniformity A) &
[z, y]
in (
block_Pervin_quasi_uniformity A) } by
A8,
A7,
Th3;
then
consider x,y be
Element of X such that
A9:
[a, b]
=
[x, y] and
A10: ex z be
Element of X st
[x, z]
in (
block_Pervin_quasi_uniformity A) &
[z, y]
in (
block_Pervin_quasi_uniformity A);
consider z be
Element of X such that
A11:
[x, z]
in (
block_Pervin_quasi_uniformity A) and
A12:
[z, y]
in (
block_Pervin_quasi_uniformity A) by
A10;
per cases ;
suppose
A13: x
in A;
[x, z]
in
[:A, A:]
proof
per cases by
A11,
XBOOLE_0:def 3;
suppose
[x, z]
in
[:(X
\ A), X:];
then x
in (X
\ A) by
ZFMISC_1: 87;
hence thesis by
A13,
XBOOLE_0:def 5;
end;
suppose
[x, z]
in
[:X, A:];
then x
in X & z
in A by
ZFMISC_1: 87;
hence thesis by
A13,
ZFMISC_1: 87;
end;
end;
then
A14: z
in A by
ZFMISC_1: 87;
[z, y]
in
[:A, A:]
proof
per cases by
A12,
XBOOLE_0:def 3;
suppose
[z, y]
in
[:(X
\ A), X:];
then z
in (X
\ A) & y
in X by
ZFMISC_1: 87;
hence thesis by
A14,
XBOOLE_0:def 5;
end;
suppose
[z, y]
in
[:X, A:];
then y
in A by
ZFMISC_1: 87;
hence thesis by
A14,
ZFMISC_1: 87;
end;
end;
then y
in A by
ZFMISC_1: 87;
then
A15:
[x, y]
in
[:X, A:] by
ZFMISC_1:def 2;
[:X, A:]
c= (
block_Pervin_quasi_uniformity A) by
XBOOLE_1: 7;
hence t
in (
block_Pervin_quasi_uniformity A) by
A8,
A9,
A15;
end;
suppose
A16: not x
in A;
per cases ;
suppose X is
empty;
hence t
in (
block_Pervin_quasi_uniformity A) by
A12;
end;
suppose X is non
empty;
then x
in (X
\ A) by
A16,
XBOOLE_0:def 5;
then
A17: t
in
[:(X
\ A), X:] by
A8,
A9,
ZFMISC_1: 87;
[:(X
\ A), X:]
c= (
block_Pervin_quasi_uniformity A) by
XBOOLE_1: 7;
hence t
in (
block_Pervin_quasi_uniformity A) by
A17;
end;
end;
end;
hence thesis;
end;
definition
let T be
TopSpace;
::
UNIFORM2:def22
func
subbasis_Pervin_quasi_uniformity (T) ->
Subset-Family of
[:the
carrier of T, the
carrier of T:] equals the set of all (
block_Pervin_quasi_uniformity O) where O be
Element of the
topology of T;
coherence
proof
the set of all (
block_Pervin_quasi_uniformity O) where O be
Element of the
topology of T
c= (
bool
[:the
carrier of T, the
carrier of T:])
proof
let x be
object;
assume x
in the set of all (
block_Pervin_quasi_uniformity O) where O be
Element of the
topology of T;
then ex O be
Element of the
topology of T st x
= (
block_Pervin_quasi_uniformity O);
hence thesis;
end;
hence thesis;
end;
end
registration
let T be non
empty
TopSpace;
cluster (
subbasis_Pervin_quasi_uniformity T) -> non
empty;
coherence
proof
(
block_Pervin_quasi_uniformity the
Element of the
topology of T)
in (
subbasis_Pervin_quasi_uniformity T);
hence thesis;
end;
end
definition
let T be
TopSpace;
::
UNIFORM2:def23
func
basis_Pervin_quasi_uniformity (T) ->
Subset-Family of
[:the
carrier of T, the
carrier of T:] equals (
FinMeetCl (
subbasis_Pervin_quasi_uniformity T));
coherence ;
end
registration
let X be
set;
cluster
cap-closed ->
quasi_basis for non
empty
Subset-Family of
[:X, X:];
coherence
proof
let SF be non
empty
Subset-Family of
[:X, X:];
assume
A1: SF is
cap-closed;
now
let b1,b2 be
Element of SF;
(b1
/\ b2)
in SF by
A1,
FINSUB_1:def 2;
hence ex b be
Element of SF st b
c= (b1
/\ b2);
end;
hence thesis;
end;
end
reserve T for
TopSpace;
registration
let T;
cluster (
basis_Pervin_quasi_uniformity T) ->
cap-closed;
coherence
proof
now
let x,y be
set;
assume that
A1: x
in (
basis_Pervin_quasi_uniformity T) and
A2: y
in (
basis_Pervin_quasi_uniformity T);
consider Y be
Subset-Family of
[:the
carrier of T, the
carrier of T:] such that
A3: Y
c= (
subbasis_Pervin_quasi_uniformity T) and
A4: Y is
finite and
A5: x
= (
Intersect Y) by
A1,
CANTOR_1:def 3;
consider Z be
Subset-Family of
[:the
carrier of T, the
carrier of T:] such that
A6: Z
c= (
subbasis_Pervin_quasi_uniformity T) 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_quasi_uniformity T) by
A3,
A6,
XBOOLE_1: 8;
hence (x
/\ y)
in (
basis_Pervin_quasi_uniformity T) by
A9,
A4,
A7,
CANTOR_1:def 3;
end;
hence thesis by
FINSUB_1:def 2;
end;
end
registration
let T;
cluster (
basis_Pervin_quasi_uniformity T) ->
quasi_basis;
coherence ;
end
registration
let T;
cluster (
basis_Pervin_quasi_uniformity T) ->
axiom_UP1;
coherence
proof
let B be
Element of (
basis_Pervin_quasi_uniformity T);
B
in (
FinMeetCl (
subbasis_Pervin_quasi_uniformity T));
then
consider Y be
Subset-Family of
[:the
carrier of T, the
carrier of T:] such that
A1: Y
c= (
subbasis_Pervin_quasi_uniformity T) and Y is
finite and
A2: B
= (
Intersect Y) by
CANTOR_1:def 3;
let t be
object;
assume
A3: t
in (
id the
carrier of T);
then
consider a,b be
object such that
A4: t
=
[a, b] by
RELAT_1:def 1;
A5: a
in the
carrier of T & a
= b by
A3,
A4,
RELAT_1:def 10;
per cases ;
suppose Y is
empty;
then B
=
[:the
carrier of T, the
carrier of T:] 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_quasi_uniformity O) where O be
Element of the
topology of T by
A1;
then
consider O be
Element of the
topology of T such that
A9: y
= (
block_Pervin_quasi_uniformity O);
A10:
[:(the
carrier of T
\ O), the
carrier of T:]
c= y &
[:the
carrier of T, O:]
c= y by
A9,
XBOOLE_1: 10;
per cases by
A5,
XBOOLE_0:def 5;
suppose a
in (the
carrier of T
\ O);
then
[a, b]
in
[:(the
carrier of T
\ O), the
carrier of T:] by
A5,
ZFMISC_1:def 2;
hence t
in y by
A4,
A10;
end;
suppose a
in O;
then
[a, b]
in
[:the
carrier of T, 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;
end
registration
let T;
cluster (
basis_Pervin_quasi_uniformity T) ->
axiom_UP3;
coherence
proof
let B1 be
Element of (
basis_Pervin_quasi_uniformity T);
B1
in (
FinMeetCl (
subbasis_Pervin_quasi_uniformity T));
then
consider Y be
Subset-Family of
[:the
carrier of T, the
carrier of T:] such that
A1: Y
c= (
subbasis_Pervin_quasi_uniformity T) and Y is
finite and
A2: B1
= (
Intersect Y) by
CANTOR_1:def 3;
per cases ;
suppose Y is
empty;
then
A3: B1
=
[:the
carrier of T, the
carrier of T:] 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_quasi_uniformity T);
take B2;
let t be
object;
assume
A6: t
in (B2
* B2);
consider a,b be
object such that
A10: t
=
[a, b] by
A6,
RELAT_1:def 1;
consider c be
object such that
A11:
[a, c]
in B2 and
A12:
[c, b]
in B2 by
A6,
A10,
RELAT_1:def 8;
thus 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_quasi_uniformity O) where O be
Element of the
topology of T by
A1;
then
consider O be
Element of the
topology of T such that
A14: Z
= (
block_Pervin_quasi_uniformity O);
[a, c]
in (
meet Y) by
A4,
A2,
SETFAM_1:def 9,
A11;
then
A15:
[a, c]
in (
block_Pervin_quasi_uniformity O) by
A14,
A13,
SETFAM_1:def 1;
[c, b]
in (
block_Pervin_quasi_uniformity O) by
A12,
A5,
A14,
A13,
SETFAM_1:def 1;
then
A16:
[a, b]
in ((
block_Pervin_quasi_uniformity O)
* (
block_Pervin_quasi_uniformity O)) by
A15,
RELAT_1:def 8;
((
block_Pervin_quasi_uniformity O)
* (
block_Pervin_quasi_uniformity O))
c= (
block_Pervin_quasi_uniformity O) by
Th20;
hence thesis by
A14,
A10,
A16;
end;
hence thesis by
A5,
A4,
SETFAM_1:def 1;
end;
end;
end;
end
definition
let T be
TopSpace;
::
UNIFORM2:def24
func
Pervin_quasi_uniformity T ->
strict
Quasi-UniformSpace equals
UniformSpaceStr (# the
carrier of T,
<.(
basis_Pervin_quasi_uniformity T).] #);
coherence by
Th11bis;
end
theorem ::
UNIFORM2:25
for T be non
empty
TopSpace, V be
Element of the
entourages of (
Pervin_quasi_uniformity T) holds ex b be
Element of (
FinMeetCl (
subbasis_Pervin_quasi_uniformity T)) st b
c= V
proof
let T be non
empty
TopSpace, V be
Element of the
entourages of (
Pervin_quasi_uniformity T);
A1:
<.(
basis_Pervin_quasi_uniformity T).]
= { x where x be
Subset of
[:the
carrier of T, the
carrier of T:] : ex b be
Element of (
basis_Pervin_quasi_uniformity T) st b
c= x } by
CARDFIL2: 14;
V
in
<.(
basis_Pervin_quasi_uniformity T).];
then ex S be
Subset of
[:the
carrier of T, the
carrier of T:] st V
= S & ex b be
Element of (
basis_Pervin_quasi_uniformity T) st b
c= S by
A1;
hence thesis;
end;
theorem ::
UNIFORM2:26
for T be non
empty
TopSpace, V be
Subset of
[:the
carrier of T, the
carrier of T:] st ex b be
Element of (
FinMeetCl (
subbasis_Pervin_quasi_uniformity T)) st b
c= V holds V is
Element of the
entourages of (
Pervin_quasi_uniformity T)
proof
let T be non
empty
TopSpace, V be
Subset of
[:the
carrier of T, the
carrier of T:];
given b be
Element of (
FinMeetCl (
subbasis_Pervin_quasi_uniformity T)) such that
A1: b
c= V;
A2:
<.(
basis_Pervin_quasi_uniformity T).]
= { x where x be
Subset of
[:the
carrier of T, the
carrier of T:] : ex b be
Element of (
basis_Pervin_quasi_uniformity T) st b
c= x } by
CARDFIL2: 14;
V
in
<.(
basis_Pervin_quasi_uniformity T).] by
A1,
A2;
hence thesis;
end;
theorem ::
UNIFORM2:27
(
subbasis_Pervin_quasi_uniformity T)
c= the
entourages of (
Pervin_quasi_uniformity T)
proof
now
let x be
object;
assume
A1: x
in (
subbasis_Pervin_quasi_uniformity T);
A2: (
subbasis_Pervin_quasi_uniformity T)
c= (
basis_Pervin_quasi_uniformity T) by
CANTOR_1: 4;
(
basis_Pervin_quasi_uniformity T)
c=
<.(
basis_Pervin_quasi_uniformity T).] by
CARDFIL2: 18;
hence x
in the
entourages of (
Pervin_quasi_uniformity T) by
A1,
A2;
end;
hence thesis;
end;
theorem ::
UNIFORM2:28
Th27: for QU be non
void
Quasi-UniformSpace holds
[:the
carrier of QU, the
carrier of QU:]
in the
entourages of QU
proof
let QU be non
void
Quasi-UniformSpace;
A1: QU is non
void;
set U = the
Element of the
entourages of QU;
U
in the
entourages of QU by
A1;
then
reconsider U as
Subset of
[:the
carrier of QU, the
carrier of QU:];
QU is
upper;
then
A2: the
entourages of QU is
upper;
[:the
carrier of QU, the
carrier of QU:]
c=
[:the
carrier of QU, the
carrier of QU:];
then
reconsider Y =
[:the
carrier of QU, the
carrier of QU:] as
Subset of
[:the
carrier of QU, the
carrier of QU:];
the
entourages of QU is non
empty by
A1;
then Y
in the
entourages of QU by
A2;
hence thesis;
end;
theorem ::
UNIFORM2:29
for QU be non
void
Quasi-UniformSpace st the
carrier of T
= the
carrier of QU & (
subbasis_Pervin_quasi_uniformity T)
c= the
entourages of QU holds the
entourages of (
Pervin_quasi_uniformity T)
c= the
entourages of QU
proof
let QU be non
void
Quasi-UniformSpace;
assume that
A2: the
carrier of T
= the
carrier of QU and
A3: (
subbasis_Pervin_quasi_uniformity T)
c= the
entourages of QU;
the
entourages of (
Pervin_quasi_uniformity T)
c= the
entourages of QU
proof
let x be
object;
assume
A4: x
in the
entourages of (
Pervin_quasi_uniformity T);
then
reconsider y = x as
Subset of
[:the
carrier of T, the
carrier of T:];
consider b be
Element of (
basis_Pervin_quasi_uniformity T) such that
A5: b
c= y by
A4,
CARDFIL2:def 8;
b
in (
FinMeetCl (
subbasis_Pervin_quasi_uniformity T));
then
consider Y be
Subset-Family of
[:the
carrier of T, the
carrier of T:] such that
A6: Y
c= (
subbasis_Pervin_quasi_uniformity T) and
A7: Y is
finite and
A8: b
= (
Intersect Y) by
CANTOR_1:def 3;
reconsider Z = Y as
finite
Subset-Family of
[:the
carrier of QU, the
carrier of QU:] by
A2,
A7;
reconsider B = the
entourages of QU as
set;
A9:
now
thus B is
Subset-Family of
[:the
carrier of QU, the
carrier of QU:];
QU is
cap-closed;
hence B is
cap-closed;
thus
[:the
carrier of QU, the
carrier of QU:]
in B by
Th27;
thus Z
c= B by
A3,
A6;
end;
QU is
upper;
then
A10: the
entourages of QU is
upper;
b is
Subset of
[:the
carrier of QU, the
carrier of QU:] & y is
Subset of
[:the
carrier of QU, the
carrier of QU:] & b
c= y & b
in the
entourages of QU by
A5,
A9,
A2,
A8,
ARMSTRNG: 1;
hence thesis by
A10;
end;
hence thesis;
end;
registration
let T be non
empty
TopSpace;
cluster (
Pervin_quasi_uniformity T) -> non
empty;
coherence ;
end
registration
let T be non
empty
TopSpace;
cluster (
Pervin_quasi_uniformity T) ->
topological;
coherence
proof
set US = (
Pervin_quasi_uniformity T), FMT =
FMT_Space_Str (# the
carrier of (
Pervin_quasi_uniformity T), (
Neighborhood (
Pervin_quasi_uniformity T)) #);
reconsider UT = FMT as non
empty
strict
FMT_Space_Str;
A1: for x be
Element of UT holds ex y be
Element of US st x
= y & (
U_FMT x)
= (
Neighborhood y)
proof
let x be
Element of UT;
(
U_FMT x)
= (the
BNbd of UT
. x) by
FINTOPO2:def 6;
then
consider y be
Element of US such that
A2: x
= y and
A3: (
U_FMT x)
= ((
Neighborhood US)
. y);
((
Neighborhood US)
. y)
= (
Neighborhood y) by
Def5;
hence thesis by
A2,
A3;
end;
now
for x be
Element of UT, V be
Element of (
U_FMT x) holds ex W be
Element of (
U_FMT x) st for y be
Element of UT st y is
Element of W holds V is
Element of (
U_FMT y)
proof
let x be
Element of UT, V be
Element of (
U_FMT x);
consider y be
Element of US such that x
= y and
A4: (
U_FMT x)
= (
Neighborhood y) by
A1;
A5: V
in (
Neighborhood y) by
A4;
then
consider V0 be
Element of the
entourages of US such that
A6: V
= (
Neighborhood (V0,y));
US is
axiom_U3;
then
consider W be
Element of the
entourages of US such that
A7: (W
* W)
c= V0;
(
Neighborhood (W,y))
in the set of all (
Neighborhood (V,y)) where V be
Element of the
entourages of US;
then
reconsider WN = (
Neighborhood (W,y)) as
Element of (
Neighborhood y);
A8: for x,y,z be
object st
[x, y]
in W &
[y, z]
in W holds
[x, z]
in V0
proof
let x,y,z be
object;
assume that
A9:
[x, y]
in W and
A10:
[y, z]
in W;
[x, z]
in (W
* W) by
A9,
A10,
RELAT_1:def 8;
hence thesis by
A7;
end;
reconsider WN as
Element of (
U_FMT x) by
A4;
take WN;
hereby
let z be
Element of UT;
assume z is
Element of WN;
then z
in { z where z be
Element of US :
[y, z]
in W };
then
consider z0 be
Element of US such that
A13: z
= z0 and
A14:
[y, z0]
in W;
consider z1 be
Element of US such that
A15: z
= z1 and
A16: (
U_FMT z)
= (
Neighborhood z1) by
A1;
A17: (
Neighborhood (W,z1))
c= (
Neighborhood (V0,y))
proof
let t be
object;
assume t
in (
Neighborhood (W,z1));
then
consider y0 be
Element of US such that
A18: t
= y0 and
A19:
[z1, y0]
in W;
[y, t]
in V0 by
A18,
A19,
A15,
A13,
A14,
A8;
hence thesis by
A18;
end;
(
Neighborhood (W,z1))
in (
Neighborhood z1);
then
reconsider WW = (
Neighborhood (W,z1)) as
Element of (
Neighborhood z1);
reconsider WW2 = WW, V2 = V as
Subset of US by
A5;
A20: WW2
c= V2 by
A6,
A17;
(
Neighborhood z1) is
upper by
Th15;
hence V is
Element of (
U_FMT z) by
A16,
A20;
end;
end;
hence UT is
U_FMT_local;
for x be
Element of UT, V be
Element of (
U_FMT x) holds x
in V
proof
let x be
Element of UT, V be
Element of (
U_FMT x);
consider y be
Element of US such that
A21: x
= y and
A22: (
U_FMT x)
= (
Neighborhood y) by
A1;
V
in the set of all (
Neighborhood (V,y)) where V be
Element of the
entourages of US by
A22;
then ex W be
Element of the
entourages of US st V
= (
Neighborhood (W,y));
hence thesis by
A21,
Th16;
end;
hence UT is
U_FMT_with_point;
for x be
Element of UT holds (
U_FMT x) is
Filter of the
carrier of UT
proof
let x be
Element of UT;
ex y be
Element of US st x
= y & (
U_FMT x)
= (
Neighborhood y) by
A1;
hence thesis by
Th18;
end;
hence UT is
U_FMT_filter;
end;
hence thesis;
end;
end
theorem ::
UNIFORM2:30
Th29: for T be non
empty
TopSpace, x be
Element of (
subbasis_Pervin_quasi_uniformity T), y be
Element of (
Pervin_quasi_uniformity T) holds { z where z be
Element of (
Pervin_quasi_uniformity T) :
[y, z]
in x }
in the
topology of T
proof
let T be non
empty
TopSpace, x be
Element of (
subbasis_Pervin_quasi_uniformity T), y be
Element of (
Pervin_quasi_uniformity T);
x
in (
subbasis_Pervin_quasi_uniformity T);
then
consider O be
Element of the
topology of T such that
A1: x
= (
block_Pervin_quasi_uniformity O);
set M = { z where z be
Element of (
Pervin_quasi_uniformity T) :
[y, z]
in x };
per cases ;
suppose
A2: y
in O;
M
= O
proof
thus M
c= O
proof
let a be
object;
assume a
in M;
then
consider b be
Element of (
Pervin_quasi_uniformity T) such that
A4: b
= a and
A5:
[y, b]
in x;
[y, b]
in
[:(the
carrier of T
\ O), the
carrier of T:] or
[y, b]
in
[:the
carrier of T, O:] by
A1,
A5,
XBOOLE_0:def 3;
then (y
in (the
carrier of T
\ O) & b
in the
carrier of T) or (y
in the
carrier of T & b
in O) by
ZFMISC_1: 87;
hence thesis by
A4,
A2,
XBOOLE_0:def 5;
end;
let a be
object;
assume
A6: a
in O;
then
reconsider b = a as
Element of (
Pervin_quasi_uniformity T);
[y, b]
in
[:the
carrier of T, O:] by
A6,
ZFMISC_1: 87;
then
[y, b]
in (
[:(the
carrier of T
\ O), the
carrier of T:]
\/
[:the
carrier of T, O:]) by
XBOOLE_0:def 3;
hence thesis by
A1;
end;
hence thesis;
end;
suppose
A7: not y
in O;
M
= the
carrier of (
Pervin_quasi_uniformity T)
proof
thus M
c= the
carrier of (
Pervin_quasi_uniformity T)
proof
let a be
object;
assume a
in M;
then ex b be
Element of (
Pervin_quasi_uniformity T) st a
= b &
[y, b]
in x;
hence thesis;
end;
let a be
object;
assume a
in the
carrier of (
Pervin_quasi_uniformity T);
then
reconsider b = a as
Element of the
carrier of (
Pervin_quasi_uniformity T);
y
in (the
carrier of T
\ O) & b
in the
carrier of T by
A7,
XBOOLE_0:def 5;
then
A10:
[y, b]
in
[:(the
carrier of T
\ O), the
carrier of T:] by
ZFMISC_1: 87;
[:(the
carrier of T
\ O), the
carrier of T:]
c= (
[:(the
carrier of T
\ O), the
carrier of T:]
\/
[:the
carrier of T, O:]) by
XBOOLE_1: 7;
hence thesis by
A1,
A10;
end;
hence thesis by
PRE_TOPC:def 1;
end;
end;
theorem ::
UNIFORM2:31
Th30: for T be non
empty
TopSpace, x be
Element of the
carrier of (
Pervin_quasi_uniformity T), b be
Element of (
FinMeetCl (
subbasis_Pervin_quasi_uniformity T)) holds { y where y be
Element of T :
[x, y]
in b }
in the
topology of T
proof
let T be non
empty
TopSpace, x be
Element of the
carrier of (
Pervin_quasi_uniformity T), b be
Element of (
FinMeetCl (
subbasis_Pervin_quasi_uniformity T));
consider Y be
Subset-Family of
[:the
carrier of (
Pervin_quasi_uniformity T), the
carrier of (
Pervin_quasi_uniformity T):] such that
A1: Y
c= (
subbasis_Pervin_quasi_uniformity T) and
A2: Y is
finite and
A3: b
= (
Intersect Y) by
CANTOR_1:def 3;
per cases ;
suppose Y is
empty;
then
A4: b
=
[:the
carrier of T, the
carrier of T:] by
A3,
SETFAM_1:def 9;
{ y where y be
Element of T :
[x, y]
in b }
= the
carrier of T
proof
thus { y where y be
Element of T :
[x, y]
in b }
c= the
carrier of T
proof
let a be
object;
assume a
in { y where y be
Element of T :
[x, y]
in b };
then ex y be
Element of T st a
= y &
[x, y]
in b;
hence thesis;
end;
let a be
object;
assume a
in the
carrier of T;
then
reconsider y = a as
Element of T;
[x, y]
in
[:the
carrier of T, the
carrier of T:];
hence thesis by
A4;
end;
hence thesis by
PRE_TOPC:def 1;
end;
suppose
A7: Y is non
empty;
then
A8: b
= (
meet Y) by
A3,
SETFAM_1:def 9;
for Y be non
empty
Subset-Family of
[:the
carrier of (
Pervin_quasi_uniformity T), the
carrier of (
Pervin_quasi_uniformity T):] st Y
c= (
subbasis_Pervin_quasi_uniformity T) & Y is
finite holds { y where y be
Element of T :
[x, y]
in (
meet Y) }
in the
topology of T
proof
let Y be non
empty
Subset-Family of
[:the
carrier of (
Pervin_quasi_uniformity T), the
carrier of (
Pervin_quasi_uniformity T):];
assume that
A9: Y
c= (
subbasis_Pervin_quasi_uniformity T) and
A10: Y is
finite;
defpred
P[
Nat] means for Z be non
empty
Subset-Family of
[:the
carrier of (
Pervin_quasi_uniformity T), the
carrier of (
Pervin_quasi_uniformity T):] st Z
c= (
subbasis_Pervin_quasi_uniformity T) & (
card Z)
= $1 holds { y where y be
Element of T :
[x, y]
in (
meet Z) }
in the
topology of T;
for Z be non
empty
Subset-Family of
[:the
carrier of (
Pervin_quasi_uniformity T), the
carrier of (
Pervin_quasi_uniformity T):] st Z
c= (
subbasis_Pervin_quasi_uniformity T) & (
card Z)
= 1 holds { y where y be
Element of T :
[x, y]
in (
meet Z) }
in the
topology of T
proof
let Z be non
empty
Subset-Family of
[:the
carrier of (
Pervin_quasi_uniformity T), the
carrier of (
Pervin_quasi_uniformity T):];
assume that
A11: Z
c= (
subbasis_Pervin_quasi_uniformity T) and
A12: (
card Z)
= 1;
consider t be
object such that
A13: Z
=
{t} by
A12,
CARD_2: 42;
reconsider y = t as
set by
TARSKI: 1;
A14: (
meet Z)
= y by
A13,
SETFAM_1: 10;
t
in (
subbasis_Pervin_quasi_uniformity T) by
A11,
A13,
ZFMISC_1: 31;
then
consider O be
Element of the
topology of T such that
A15: t
= (
block_Pervin_quasi_uniformity O);
per cases ;
suppose
A16: x
in O;
{ y where y be
Element of T :
[x, y]
in (
meet Z) }
in the
topology of T
proof
A17: { z where z be
Element of T :
[x, z]
in (
block_Pervin_quasi_uniformity O) }
= O
proof
A18: { z where z be
Element of T :
[x, z]
in (
block_Pervin_quasi_uniformity O) }
c= O
proof
let a be
object;
assume a
in { z where z be
Element of T :
[x, z]
in (
block_Pervin_quasi_uniformity O) };
then ex z be
Element of T st a
= z &
[x, z]
in (
block_Pervin_quasi_uniformity O);
then
[x, a]
in
[:(the
carrier of T
\ O), the
carrier of T:] or
[x, a]
in
[:the
carrier of T, O:] by
XBOOLE_0:def 3;
then (x
in (the
carrier of T
\ O) & a
in the
carrier of T) or (x
in the
carrier of T & a
in O) by
ZFMISC_1: 87;
hence thesis by
A16,
XBOOLE_0:def 5;
end;
O
c= { z where z be
Element of T :
[x, z]
in (
block_Pervin_quasi_uniformity O) }
proof
let a be
object;
assume
A19: a
in O;
then
reconsider b = a as
Element of T;
[x, a]
in
[:the
carrier of T, O:] by
A19,
ZFMISC_1: 87;
then
[x, b]
in (
block_Pervin_quasi_uniformity O) by
XBOOLE_0:def 3;
hence thesis;
end;
hence thesis by
A18;
end;
thus thesis by
A15,
A14,
A17;
end;
hence thesis;
end;
suppose
A20: not x
in O;
{ z where z be
Element of T :
[x, z]
in (
block_Pervin_quasi_uniformity O) }
= the
carrier of T
proof
thus { z where z be
Element of T :
[x, z]
in (
block_Pervin_quasi_uniformity O) }
c= the
carrier of T
proof
let a be
object;
assume a
in { z where z be
Element of T :
[x, z]
in (
block_Pervin_quasi_uniformity O) };
then ex z be
Element of T st a
= z &
[x, z]
in (
block_Pervin_quasi_uniformity O);
hence thesis;
end;
let a be
object;
assume a
in the
carrier of T;
then
reconsider b = a as
Element of T;
x
in (the
carrier of T
\ O) by
A20,
XBOOLE_0:def 5;
then
[x, b]
in
[:(the
carrier of T
\ O), the
carrier of T:] or
[x, b]
in
[:the
carrier of T, O:] by
ZFMISC_1: 87;
then
[x, b]
in (
block_Pervin_quasi_uniformity O) by
XBOOLE_0:def 3;
hence thesis;
end;
hence thesis by
A15,
A14,
PRE_TOPC:def 1;
end;
end;
then
A22:
P[1];
A23: for k be non
zero
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be non
zero
Nat;
assume
A24:
P[k];
now
let Z be non
empty
Subset-Family of
[:the
carrier of (
Pervin_quasi_uniformity T), the
carrier of (
Pervin_quasi_uniformity T):];
assume that
A25: Z
c= (
subbasis_Pervin_quasi_uniformity T) and
A26: (
card Z)
= (k
+ 1);
set z = the
Element of Z;
A27: (
card (Z
\
{z}))
= k by
A26,
STIRL2_1: 55;
then
A28: (Z
\
{z}) is non
empty;
(Z
\
{z})
c= Z by
XBOOLE_1: 36;
then
A29: (Z
\
{z})
c= (
subbasis_Pervin_quasi_uniformity T) by
A25;
(Z
\
{z}) is non
empty
Subset-Family of
[:the
carrier of (
Pervin_quasi_uniformity T), the
carrier of (
Pervin_quasi_uniformity T):] by
A27;
then
A30: { y where y be
Element of T :
[x, y]
in (
meet (Z
\
{z})) }
in the
topology of T by
A24,
A27,
A29;
A31: ({ y where y be
Element of T :
[x, y]
in (
meet (Z
\
{z})) }
/\ { y where y be
Element of T :
[x, y]
in z })
= { y where y be
Element of T :
[x, y]
in (
meet Z) }
proof
set M1 = { y where y be
Element of T :
[x, y]
in (
meet (Z
\
{z})) }, M2 = { y where y be
Element of T :
[x, y]
in z }, M3 = { y where y be
Element of T :
[x, y]
in (
meet Z) };
A32: (M1
/\ M2)
c= M3
proof
let a be
object;
assume a
in (M1
/\ M2);
then
A33: a
in M1 & a
in M2 by
XBOOLE_0:def 4;
then
consider b be
Element of T such that
A34: a
= b and
A35:
[x, b]
in (
meet (Z
\
{z}));
consider c be
Element of T such that
A36: a
= c and
A37:
[x, c]
in z by
A33;
now
let Y be
set;
assume Y
in Z;
per cases ;
suppose Y
in Z & not Y
in
{z};
then Y
in (Z
\
{z}) by
XBOOLE_0:def 5;
hence
[x, b]
in Y by
A35,
SETFAM_1:def 1;
end;
suppose Y
in
{z};
hence
[x, b]
in Y by
A34,
A36,
A37,
TARSKI:def 1;
end;
end;
then
[x, b]
in (
meet Z) by
SETFAM_1:def 1;
hence thesis by
A34;
end;
M3
c= (M1
/\ M2)
proof
let a be
object;
assume a
in M3;
then
consider b be
Element of T such that
A38: a
= b and
A39:
[x, b]
in (
meet Z);
now
let Y be
set;
assume
A40: Y
in (Z
\
{z});
(Z
\
{z})
c= Z by
XBOOLE_1: 36;
hence
[x, b]
in Y by
A40,
A39,
SETFAM_1:def 1;
end;
then
[x, b]
in (
meet (Z
\
{z})) by
A28,
SETFAM_1:def 1;
then
A41: b
in M1;
[x, b]
in z by
A39,
SETFAM_1:def 1;
then a
in M2 by
A38;
hence thesis by
A41,
A38,
XBOOLE_0:def 4;
end;
hence thesis by
A32;
end;
z
in (
subbasis_Pervin_quasi_uniformity T) by
A25;
then { y where y be
Element of T :
[x, y]
in z }
in the
topology of T by
Th29;
hence { y where y be
Element of T :
[x, y]
in (
meet Z) }
in the
topology of T by
A31,
A30,
PRE_TOPC:def 1;
end;
hence thesis;
end;
A42: for k be non
zero
Nat holds
P[k] from
NAT_1:sch 10(
A22,
A23);
ex n be
Nat st (
card Y)
= n by
A10;
hence thesis by
A9,
A42;
end;
hence thesis by
A8,
A1,
A2,
A7;
end;
end;
theorem ::
UNIFORM2:32
Th31: for UT be non
empty
strict
Quasi-UniformSpace, FMT be non
empty
strict
FMT_Space_Str, x be
Element of FMT st FMT
=
FMT_Space_Str (# the
carrier of UT, (
Neighborhood UT) #) holds ex y be
Element of UT st x
= y & (
U_FMT x)
= (
Neighborhood y)
proof
let UT be non
empty
strict
Quasi-UniformSpace, FMT be non
empty
strict
FMT_Space_Str, x be
Element of FMT;
assume
A1: FMT
=
FMT_Space_Str (# the
carrier of UT, (
Neighborhood UT) #);
(
U_FMT x)
= (the
BNbd of FMT
. x) by
FINTOPO2:def 6;
then
consider y be
Element of UT such that
A2: x
= y and
A3: (
U_FMT x)
= ((
Neighborhood UT)
. y) by
A1;
((
Neighborhood UT)
. y)
= (
Neighborhood y) by
Def5;
hence thesis by
A2,
A3;
end;
theorem ::
UNIFORM2:33
Th32: for T be non
empty
TopSpace holds (
Family_open_set (
FMT_induced_by (
Pervin_quasi_uniformity T)))
= the
topology of T
proof
let T be non
empty
TopSpace;
A1: (
Family_open_set (
FMT_induced_by (
Pervin_quasi_uniformity T)))
c= the
topology of T
proof
let x be
object;
assume x
in (
Family_open_set (
FMT_induced_by (
Pervin_quasi_uniformity T)));
then
consider O be
open
Subset of (
FMT_induced_by (
Pervin_quasi_uniformity T)) such that
A2: x
= O;
reconsider O1 = O as
Subset of T;
for x be
set holds x
in O1 iff ex B be
Subset of T st B is
open & B
c= O1 & x
in B
proof
let x be
set;
hereby
assume
A3: x
in O1;
then
reconsider t = x as
Element of (
FMT_induced_by (
Pervin_quasi_uniformity T));
consider y be
Element of the
carrier of (
Pervin_quasi_uniformity T) such that
A4: t
= y and
A5: (
U_FMT t)
= (
Neighborhood y) by
Th31;
O
in (
Neighborhood y) by
A5,
FINTOPO7:def 1,
A3;
then
consider V be
Element of the
entourages of (
Pervin_quasi_uniformity T) such that
A6: O
= (
Neighborhood (V,y));
consider b be
Element of (
FinMeetCl (
subbasis_Pervin_quasi_uniformity T)) such that
A7: b
c= V by
CARDFIL2:def 8;
(
FinMeetCl (
subbasis_Pervin_quasi_uniformity T))
c=
<.(
FinMeetCl (
subbasis_Pervin_quasi_uniformity T)).] by
CARDFIL2: 18;
then
A16: b
in the
entourages of (
Pervin_quasi_uniformity T);
A17:
[y, y]
in (
id the
carrier of (
Pervin_quasi_uniformity T)) by
RELAT_1:def 10;
(
Pervin_quasi_uniformity T) is
axiom_U1;
then
A18: (
id the
carrier of (
Pervin_quasi_uniformity T))
c= b by
A16;
reconsider B = { z where z be
Element of the
carrier of (
Pervin_quasi_uniformity T) :
[y, z]
in b } as
set;
B
c= the
carrier of (
Pervin_quasi_uniformity T)
proof
let t be
object;
assume t
in B;
then ex z be
Element of T st t
= z &
[y, z]
in b;
hence thesis;
end;
then
reconsider B as
Subset of T;
now
take B;
thus B is
open by
Th30,
PRE_TOPC:def 2;
B
c= O
proof
let t be
object;
assume t
in B;
then ex z be
Element of T st t
= z &
[y, z]
in b;
hence thesis by
A7,
A6;
end;
hence B
c= O1;
thus x
in B by
A4,
A18,
A17;
end;
hence ex B be
Subset of T st B is
open & B
c= O1 & x
in B;
end;
assume ex B be
Subset of T st B is
open & B
c= O1 & x
in B;
hence x
in O1;
end;
hence thesis by
A2,
PRE_TOPC:def 2,
TOPS_1: 25;
end;
the
topology of T
c= (
Family_open_set (
FMT_induced_by (
Pervin_quasi_uniformity T)))
proof
let x be
object;
assume
A20: x
in the
topology of T;
then
reconsider y = x as
Subset of T;
reconsider z = y as
Subset of (
Pervin_quasi_uniformity T);
for u be
Element of (
FMT_induced_by (
Pervin_quasi_uniformity T)) st u
in z holds z
in (
U_FMT u)
proof
let u be
Element of (
FMT_induced_by (
Pervin_quasi_uniformity T));
assume
A21: u
in z;
consider w be
Element of the
carrier of (
Pervin_quasi_uniformity T) such that
A22: u
= w and
A23: (
U_FMT u)
= (
Neighborhood w) by
Th31;
reconsider W = (
block_Pervin_quasi_uniformity y) as
Subset of
[:the
carrier of (
Pervin_quasi_uniformity T), the
carrier of (
Pervin_quasi_uniformity T):];
A24: W
in (
subbasis_Pervin_quasi_uniformity T) by
A20;
A25: (
subbasis_Pervin_quasi_uniformity T)
c= (
FinMeetCl (
subbasis_Pervin_quasi_uniformity T)) by
CANTOR_1: 4;
(
FinMeetCl (
subbasis_Pervin_quasi_uniformity T))
c=
<.(
FinMeetCl (
subbasis_Pervin_quasi_uniformity T)).] by
CARDFIL2: 18;
then
reconsider W as
Element of the
entourages of (
Pervin_quasi_uniformity T) by
A25,
A24;
{ ww where ww be
Element of T :
[w, ww]
in (
block_Pervin_quasi_uniformity y) }
= y
proof
thus { ww where ww be
Element of T :
[w, ww]
in (
block_Pervin_quasi_uniformity y) }
c= y
proof
let a be
object;
assume a
in { ww where ww be
Element of T :
[w, ww]
in (
block_Pervin_quasi_uniformity y) };
then
consider ww be
Element of T such that
A27: a
= ww and
A28:
[w, ww]
in (
[:(the
carrier of T
\ y), the
carrier of T:]
\/
[:the
carrier of T, y:]);
[w, ww]
in
[:(the
carrier of T
\ y), the
carrier of T:] or
[w, ww]
in
[:the
carrier of T, y:] by
A28,
XBOOLE_0:def 3;
then (w
in (the
carrier of T
\ y) & ww
in the
carrier of T) or (w
in the
carrier of T & ww
in y) by
ZFMISC_1: 87;
hence thesis by
A27,
A21,
A22,
XBOOLE_0:def 5;
end;
let a be
object;
assume
A29: a
in y;
then
reconsider b = a as
Element of T;
[w, b]
in
[:the
carrier of T, y:] by
A29,
ZFMISC_1: 87;
then
[w, b]
in (
block_Pervin_quasi_uniformity y) by
XBOOLE_0:def 3;
hence thesis;
end;
then z
= (
Neighborhood (W,w));
hence thesis by
A23;
end;
then z is
open
Subset of (
FMT_induced_by (
Pervin_quasi_uniformity T)) by
FINTOPO7:def 1;
hence thesis;
end;
hence thesis by
A1;
end;
theorem ::
UNIFORM2:34
for T be non
empty
strict
TopSpace holds (
TopSpace_induced_by (
Pervin_quasi_uniformity T))
= T
proof
let T be non
empty
strict
TopSpace;
the
topology of (
TopSpace_induced_by (
Pervin_quasi_uniformity T))
= (
Family_open_set (
FMT_induced_by (
Pervin_quasi_uniformity T))) by
FINTOPO7:def 16;
hence thesis by
FINTOPO7:def 16,
Th32;
end;