:: Quasi-uniform Space
:: by Roland Coghetto
::
:: Received June 30, 2016
:: Copyright (c) 2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies EQREL_1, YELLOW_6, FINTOPO7, SIMPLEX0, FINTOPO2, RELAT_2,
PRE_TOPC, FUNCT_1, STRUCT_0, CARD_1, XBOOLE_0, SUBSET_1, SETFAM_1,
TARSKI, ZFMISC_1, RELAT_1, CARD_FIL, WAYBEL_0, ARYTM_3, CANTOR_1,
FILTER_0, XXREAL_1, PCOMPS_1, RCOMP_1, FINSUB_1, PARTFUN1, TEX_1,
FINSET_1, TOLER_1, NAT_1, XCMPLX_0, UNIFORM2, FINSEQ_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
RELAT_2, ORDINAL1, RELSET_1, PARTFUN1, MCART_1, FUNCT_2, DOMAIN_1,
CANTOR_1, FINSET_1, NAT_1, SIMPLEX0, CARD_FIL, EQREL_1, TEX_1, STRUCT_0,
CARDFIL2, FINSUB_1, FINTOPO2, FINTOPO7, TOLER_1, PRE_TOPC, CARD_1;
constructors NAT_1, CARDFIL2, TOPMETR, FINSUB_1, FINTOPO7, CANTOR_1, TEX_1;
registrations CARD_1, PARTFUN1, RELAT_1, ZFMISC_1, XBOOLE_0, SUBSET_1,
ORDINAL1, RELSET_1, STRUCT_0, FINTOPO7, PRE_TOPC, CANTOR_1, FINSET_1;
requirements NUMERALS, SUBSET, BOOLE;
begin :: Preliminaries
reserve X for set,
A for Subset of X,
R,S for Relation of X;
theorem :: UNIFORM2:1
[:X \ A,X:] \/ [:X,A:] c= [:X,X:];
theorem :: UNIFORM2:2
[:X \ A,X:] \/ [:X,A:] = [:A,A:] \/ [:X \ A,X:];
theorem :: UNIFORM2:3
R * S = {[x,y] where x,y is Element of X : ex z being Element of X st
[x,z] in R & [z,y] in S};
registration
let X be set, cB be Subset-Family of X;
cluster <.cB.] -> non empty;
end;
registration
let X be set, cB be Subset-Family of [:X,X:];
cluster -> Relation-like for Element of cB;
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;
redefine func B[~] -> Subset of [:X,X:];
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;
redefine func B1 [*] B2 -> Subset of [:X,X:];
end;
theorem :: UNIFORM2:4
for X being set,G being Subset-Family of X st G is upper holds
FinMeetCl G is upper;
theorem :: UNIFORM2:5
R is_symmetric_in X implies R~ is_symmetric_in X;
begin :: Uniform Space Structure
definition
struct (1-sorted)
UniformSpaceStr
(# carrier -> set,
entourages -> Subset-Family of [:the carrier,the carrier:] #);
end;
definition
let U be UniformSpaceStr;
attr U is void means
:: UNIFORM2:def 1
the entourages of U is empty;
end;
definition
let X be set;
func Uniform_Space(X) -> strict UniformSpaceStr equals
:: UNIFORM2:def 2
UniformSpaceStr (# X , {} bool[:X,X:] #);
end;
definition
func TrivialUniformSpace -> strict UniformSpaceStr equals
:: UNIFORM2:def 3
UniformSpaceStr (# {} , cobool[:{},{}:] #);
func NonEmptyTrivialUniformSpace -> strict UniformSpaceStr means
:: UNIFORM2:def 4
ex SF being Subset-Family of [:{{}},{{}}:] st SF = {[:{{}},{{}}:]} &
it = UniformSpaceStr (#{{}},SF#);
end;
registration
let X be empty set;
cluster Uniform_Space(X) -> empty;
end;
registration
let X be non empty set;
cluster Uniform_Space(X) -> non empty;
end;
registration
let X be set;
cluster Uniform_Space(X) -> void;
end;
registration
cluster TrivialUniformSpace -> empty non void;
cluster NonEmptyTrivialUniformSpace -> non empty non void;
end;
registration
cluster empty strict void for UniformSpaceStr;
cluster empty strict non void for UniformSpaceStr;
cluster non empty strict void for UniformSpaceStr;
cluster non empty strict non void for UniformSpaceStr;
end;
definition
let X be set, SF be Subset-Family of [:X,X:];
func SF[~] -> Subset-Family of [:X,X:] equals
:: UNIFORM2:def 5
the set of all S[~] where S is Element of SF;
end;
definition
let US be UniformSpaceStr;
func US[~] -> UniformSpaceStr equals
:: UNIFORM2:def 6
UniformSpaceStr(# the carrier of US, (the entourages of US)[~] #);
end;
registration
let USS be non empty UniformSpaceStr;
cluster USS[~] -> non empty;
end;
begin :: Axioms
definition
let US be UniformSpaceStr;
attr US is upper means
:: UNIFORM2:def 7
the entourages of US is upper;
attr US is cap-closed means
:: UNIFORM2:def 8
the entourages of US is cap-closed;
attr US is axiom_U1 means
:: UNIFORM2:def 9
for S being Element of the entourages of US holds
id the carrier of US c= S;
attr US is axiom_U2 means
:: UNIFORM2:def 10
for S being Element of the entourages of US holds
S[~] in the entourages of US;
attr US is axiom_U3 means
:: UNIFORM2:def 11
for S being Element of the entourages of US holds
ex W being Element of the entourages of US st W [*] W c= S;
end;
theorem :: UNIFORM2:6
for US being non void UniformSpaceStr holds
US is axiom_U1 iff for S being Element of the entourages of US holds
ex R being Relation of the carrier of US st R = S &
R is_reflexive_in the carrier of US;
theorem :: UNIFORM2:7
for US being non void UniformSpaceStr holds
US is axiom_U1 iff for S being Element of the entourages of US
ex R being total reflexive Relation of the carrier of US st R = S;
registration
cluster void -> non axiom_U2 for UniformSpaceStr;
end;
theorem :: UNIFORM2:8
for US being UniformSpaceStr st US is axiom_U2 holds
for S being Element of the entourages of US holds
(for x,y being Element of US st [x,y] in S holds
[y,x] in union the entourages of US);
theorem :: UNIFORM2:9
for US being non void UniformSpaceStr st
for S being Element of the entourages of US holds
ex R being Relation of the carrier of US st S = R &
R is_symmetric_in the carrier of US holds US is axiom_U2;
theorem :: UNIFORM2:10
for US being non void UniformSpaceStr st
for S being Element of the entourages of US holds
ex R being Relation of the carrier of US st S = R &
R is symmetric holds US is axiom_U2;
theorem :: UNIFORM2:11
for US being non void UniformSpaceStr st
for S being Element of the entourages of US holds
ex R being Tolerance of the carrier of US st S = R holds US is axiom_U1 &
US is axiom_U2;
registration
let X be empty set;
cluster Uniform_Space(X) ->
upper cap-closed axiom_U1 non axiom_U2 axiom_U3;
end;
registration
cluster Uniform_Space{{}} -> upper cap-closed non axiom_U2;
cluster TrivialUniformSpace -> upper cap-closed axiom_U1 axiom_U2 axiom_U3;
cluster NonEmptyTrivialUniformSpace ->
upper cap-closed axiom_U1 axiom_U2 axiom_U3;
end;
registration
cluster strict empty non void upper cap-closed axiom_U1 axiom_U2 axiom_U3
for UniformSpaceStr;
end;
registration
cluster empty -> axiom_U1 for strict UniformSpaceStr;
end;
registration
cluster strict non empty non void upper cap-closed axiom_U1 axiom_U2 axiom_U3
for UniformSpaceStr;
end;
definition
let SUS be non empty axiom_U1 UniformSpaceStr,
x be Element of SUS,
V be Element of the entourages of SUS;
func Neighborhood(V,x) -> non empty Subset of SUS equals
:: UNIFORM2:def 12
{y where y is Element of SUS: [x,y] in V};
end;
theorem :: UNIFORM2:12
for USS being non empty axiom_U1 UniformSpaceStr, x being Element of
the carrier of USS, V being Element of the entourages of USS holds
x in Neighborhood(V,x);
definition
let USS be cap-closed UniformSpaceStr,
V1,V2 be Element of the entourages of USS;
redefine func V1 /\ V2 -> Element of the entourages of USS;
end;
theorem :: UNIFORM2:13
for USS being non empty cap-closed axiom_U1 UniformSpaceStr,
x being Element of USS,
V,W being Element of the entourages of USS holds
Neighborhood(V,x) /\ Neighborhood(W,x) = Neighborhood(V /\ W,x);
registration
let USS be non empty axiom_U1 UniformSpaceStr;
cluster the entourages of USS -> with_non-empty_elements;
end;
registration
let USS be non empty axiom_U1 UniformSpaceStr;
cluster the entourages of USS -> non empty;
end;
definition
let USS be non empty axiom_U1 UniformSpaceStr,x being Point of USS;
func Neighborhood(x) -> Subset-Family of USS equals
:: UNIFORM2:def 13
the set of all Neighborhood(V,x) where V is Element of the entourages of USS;
end;
registration
let USS be non empty axiom_U1 UniformSpaceStr,x being Point of USS;
cluster Neighborhood(x) -> non empty;
end;
theorem :: UNIFORM2:14
for SUS being non empty axiom_U1 UniformSpaceStr, x being Element of
the carrier of SUS, V being 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);
definition
let USS be non empty axiom_U1 UniformSpaceStr;
func Neighborhood(USS) -> Function of the carrier of USS,bool bool
the carrier of USS means
:: UNIFORM2:def 14
for x being Element of USS holds it.x = Neighborhood(x);
end;
definition
let USS be non empty axiom_U1 UniformSpaceStr;
attr USS is topological means
:: UNIFORM2:def 15
FMT_Space_Str(# the carrier of USS,Neighborhood(USS) #) is FMT_TopSpace;
end;
begin :: Quasi-Uniform Space
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[~] = {{}};
theorem :: UNIFORM2:16
the entourages of QUS[~] = {{}} & the entourages of QUS[~] is upper
implies the carrier of QUS is empty;
registration
let QUS be non void Quasi-UniformSpace;
cluster QUS[~] -> upper cap-closed axiom_U1 axiom_U3;
end;
definition
let X be set, cB be Subset-Family of [:X,X:];
attr cB is axiom_UP1 means
:: UNIFORM2:def 16
for B being Element of cB holds id X c= B;
attr cB is axiom_UP3 means
:: UNIFORM2:def 17
for B1 being Element of cB ex B2 being Element of cB st B2 [*] B2 c= B1;
end;
theorem :: UNIFORM2:17
for X being non empty set,cB being empty Subset-Family of [:X,X:] holds
not cB is axiom_UP1;
theorem :: UNIFORM2:18
for X being set,cB being 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;
begin :: Semi-Uniform space
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;
end;
theorem :: UNIFORM2:19
SUS is empty implies {} in the entourages of SUS;
registration
let SUS be empty Semi-UniformSpace;
cluster the entourages of SUS -> with_empty_element;
end;
begin :: Locally Uniform Space
definition
let SUS be non empty Semi-UniformSpace;
attr SUS is axiom_UL means
:: UNIFORM2:def 18
for S being Element of the entourages of SUS,
x being Element of SUS holds
ex W being Element of the entourages of SUS st
{y where y is Element of SUS: [x,y] in W [*] W} c= Neighborhood(S,x);
end;
registration
cluster axiom_U3 -> axiom_UL for non empty Semi-UniformSpace;
end;
registration
cluster axiom_UL for non empty Semi-UniformSpace;
end;
definition
mode Locally-UniformSpace is axiom_UL non empty Semi-UniformSpace;
end;
theorem :: UNIFORM2:20
for USS being non empty upper axiom_U1 UniformSpaceStr, x being Element of
the carrier of USS holds Neighborhood(x) is upper;
theorem :: UNIFORM2:21
for US being non empty axiom_U1 UniformSpaceStr,
x being Element of US,
V being Element of the entourages of US holds x in Neighborhood(V,x);
theorem :: UNIFORM2:22
for US being non empty cap-closed axiom_U1 UniformSpaceStr,
x being Element of US holds Neighborhood(x) is cap-closed;
theorem :: UNIFORM2:23
for US being non empty upper cap-closed axiom_U1 UniformSpaceStr,
x being Element of US holds
Neighborhood(x) is Filter of the carrier of US;
registration
cluster -> topological for Locally-UniformSpace;
end;
begin :: Topological Space induced by a Uniform Space Structure
definition
let USS be topological non empty axiom_U1 UniformSpaceStr;
func FMT_induced_by(USS) -> non empty strict FMT_TopSpace equals
:: UNIFORM2:def 19
FMT_Space_Str(# the carrier of USS,Neighborhood(USS) #);
end;
definition
let USS be topological non empty axiom_U1 UniformSpaceStr;
func TopSpace_induced_by(USS) -> TopSpace equals
:: UNIFORM2:def 20
FMT2TopSpace FMT_induced_by(USS);
end;
begin :: The quasi-uniform Pervin Space induced by a topological space
definition
let X be set, A be Subset of X;
func block_Pervin_quasi_uniformity(A) -> Subset of [:X,X:] equals
:: UNIFORM2:def 21
[:X \ A,X:] \/ [:X,A:];
end;
theorem :: UNIFORM2:24
id X c= block_Pervin_quasi_uniformity(A) &
(block_Pervin_quasi_uniformity(A)) * (block_Pervin_quasi_uniformity(A))
c= block_Pervin_quasi_uniformity(A);
definition
let T be TopSpace;
func subbasis_Pervin_quasi_uniformity(T) ->
Subset-Family of [:the carrier of T,the carrier of T:] equals
:: UNIFORM2:def 22
the set of all block_Pervin_quasi_uniformity(O) where
O is Element of the topology of T;
end;
registration
let T be non empty TopSpace;
cluster subbasis_Pervin_quasi_uniformity(T) -> non empty;
end;
definition
let T be TopSpace;
func basis_Pervin_quasi_uniformity(T) -> Subset-Family of
[:the carrier of T,the carrier of T:] equals
:: UNIFORM2:def 23
FinMeetCl(subbasis_Pervin_quasi_uniformity(T));
end;
registration
let X be set;
cluster cap-closed -> quasi_basis for non empty Subset-Family of [:X,X:];
end;
reserve T for TopSpace;
registration
let T;
cluster basis_Pervin_quasi_uniformity(T) -> cap-closed;
end;
registration
let T;
cluster basis_Pervin_quasi_uniformity(T) -> quasi_basis;
end;
registration
let T;
cluster basis_Pervin_quasi_uniformity(T) -> axiom_UP1;
end;
registration
let T;
cluster basis_Pervin_quasi_uniformity(T) -> axiom_UP3;
end;
definition
let T be TopSpace;
func Pervin_quasi_uniformity T -> strict Quasi-UniformSpace equals
:: UNIFORM2:def 24
UniformSpaceStr(# the carrier of T,<.basis_Pervin_quasi_uniformity(T).] #);
end;
theorem :: UNIFORM2:25
for T being non empty TopSpace, V being Element of the entourages of
Pervin_quasi_uniformity T ex b being Element of
FinMeetCl(subbasis_Pervin_quasi_uniformity(T)) st b c= V;
theorem :: UNIFORM2:26
for T being non empty TopSpace, V being Subset of
[:the carrier of T,the carrier of T:] st ex b being Element of
FinMeetCl(subbasis_Pervin_quasi_uniformity(T)) st b c= V
holds V is Element of the entourages of Pervin_quasi_uniformity T;
theorem :: UNIFORM2:27
subbasis_Pervin_quasi_uniformity(T) c=
the entourages of Pervin_quasi_uniformity T;
theorem :: UNIFORM2:28
for QU being non void Quasi-UniformSpace holds
[:the carrier of QU,the carrier of QU:] in the entourages of QU;
theorem :: UNIFORM2:29
for QU being 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;
registration
let T be non empty TopSpace;
cluster Pervin_quasi_uniformity T -> non empty;
end;
registration
let T be non empty TopSpace;
cluster Pervin_quasi_uniformity T -> topological;
end;
theorem :: UNIFORM2:30
for T being non empty TopSpace, x being Element of
subbasis_Pervin_quasi_uniformity(T),
y being Element of Pervin_quasi_uniformity T holds
{z where z is Element of Pervin_quasi_uniformity T:
[y,z] in x} in the topology of T;
theorem :: UNIFORM2:31
for T being non empty TopSpace,x being Element of the carrier of
Pervin_quasi_uniformity T, b being Element of
FinMeetCl(subbasis_Pervin_quasi_uniformity(T)) holds
{y where y is Element of T:[x,y] in b} in the topology of T;
theorem :: UNIFORM2:32
for UT being non empty strict Quasi-UniformSpace,
FMT being non empty strict FMT_Space_Str, x being Element of FMT st
FMT = FMT_Space_Str(#the carrier of UT,Neighborhood(UT) #) holds
ex y being Element of UT st x = y &
U_FMT x = Neighborhood y;
theorem :: UNIFORM2:33
for T being non empty TopSpace holds
Family_open_set(FMT_induced_by(Pervin_quasi_uniformity T)) =
the topology of T;
theorem :: UNIFORM2:34
for T being non empty strict TopSpace holds
TopSpace_induced_by(Pervin_quasi_uniformity T) = T;