:: Quasi-uniform Space :: by Roland Coghetto :: :: Received June 30, 2016 :: Copyright (c) 2016-2021 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;