:: Moore-Smith Convergence
:: by Andrzej Trybulec
::
:: Received November 12, 1996
:: Copyright (c) 1996-2017 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 CLASSES2, CLASSES1, ORDINAL1, XBOOLE_0, FUNCT_1, RELAT_1, TARSKI,
CARD_3, CARD_1, FUNCT_2, PRALG_1, PBOOLE, SUBSET_1, RLVECT_2, STRUCT_0,
FUNCOP_1, WAYBEL_3, YELLOW_1, ORDERS_2, WAYBEL_0, XXREAL_0, RELAT_2,
ZFMISC_1, CAT_1, YELLOW_0, WELLORD1, PRE_TOPC, RCOMP_1, CONNSP_2,
COMPTS_1, MCART_1, TOPS_1, SEQ_2, ORDINAL2, SETFAM_1, YELLOW_6;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, MCART_1,
RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, CARD_1,
CARD_3, FUNCOP_1, ORDINAL1, CLASSES1, CLASSES2, TOLER_1, STRUCT_0,
TOPS_1, COMPTS_1, CONNSP_2, PRALG_1, ORDERS_2, LATTICE3, PRE_TOPC,
YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_3, WAYBEL_3;
constructors BINOP_1, CLASSES1, TOLER_1, CLASSES2, REALSET1, TOPS_1, COMPTS_1,
CONNSP_2, LATTICE3, PRALG_1, YELLOW_3, WAYBEL_3, RELSET_1, PBOOLE,
XTUPLE_0, WAYBEL_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1,
CARD_1, CLASSES1, CARD_3, CLASSES2, PBOOLE, STRUCT_0, ORDERS_2, PCOMPS_1,
LATTICE3, YELLOW_0, WAYBEL_0, PARTFUN1, YELLOW_1, YELLOW_3, WAYBEL_3,
RELSET_1, TOPS_1, RELAT_1, XTUPLE_0;
requirements BOOLE, SUBSET;
begin :: Preliminaries, classical mathematics
reserve x,y,z,X for set,
T for Universe;
definition
let X;
func the_universe_of X -> set equals
:: YELLOW_6:def 1
Tarski-Class the_transitive-closure_of X;
end;
registration
let X;
cluster the_universe_of X -> epsilon-transitive Tarski;
end;
registration
let X;
cluster the_universe_of X -> universal non empty;
end;
theorem :: YELLOW_6:1
for f being Function st dom f in T & rng f c= T holds product f in T;
begin
begin :: 1-sorted structures
theorem :: YELLOW_6:2
for Y be non empty set for J being 1-sorted-yielding
ManySortedSet of Y, i being Element of Y holds (Carrier J).i = the carrier of J
.i;
registration
cluster non empty constant 1-sorted-yielding for Function;
end;
notation
let J be 1-sorted-yielding Function;
synonym J is yielding_non-empty_carriers for J is non-Empty;
end;
definition
let J be 1-sorted-yielding Function;
redefine attr J is yielding_non-empty_carriers means
:: YELLOW_6:def 2
for i being set st i in rng J holds i is non empty 1-sorted;
end;
registration
let X be set;
let L be 1-sorted;
cluster X --> L -> 1-sorted-yielding;
end;
registration
let I be set;
cluster yielding_non-empty_carriers for
1-sorted-yielding ManySortedSet of I;
end;
registration
let I be non empty set;
let J be RelStr-yielding ManySortedSet of I;
cluster the carrier of product J -> functional;
end;
registration
let I be set;
let J be yielding_non-empty_carriers 1-sorted-yielding ManySortedSet of I;
cluster Carrier J -> non-empty;
end;
begin :: Preliminaries to Relational Structures
registration
let T be non empty RelStr, A be lower Subset of T;
cluster A` -> upper;
end;
registration
let T be non empty RelStr, A be upper Subset of T;
cluster A` -> lower;
end;
definition
let N be non empty RelStr;
redefine attr N is directed means
:: YELLOW_6:def 3
for x,y being Element of N ex z being Element of N st x <= z & y <= z;
end;
registration
let X be set;
cluster BoolePoset X -> directed;
end;
registration
cluster non empty directed transitive strict for RelStr;
end;
registration
let I be set;
cluster yielding_non-empty_carriers for RelStr-yielding ManySortedSet of I;
end;
registration
let I be non empty set;
let J be yielding_non-empty_carriers RelStr-yielding ManySortedSet of I;
cluster product J -> non empty;
end;
registration
let Y1,Y2 be directed RelStr;
cluster [:Y1,Y2:] -> directed;
end;
theorem :: YELLOW_6:3
for R being RelStr holds the carrier of R = the carrier of R~;
definition
let S be 1-sorted, N be NetStr over S;
attr N is constant means
:: YELLOW_6:def 4
the mapping of N is constant;
end;
definition
let R be RelStr, T be non empty 1-sorted, p be Element of T;
func ConstantNet(R,p) -> strict NetStr over T means
:: YELLOW_6:def 5
the RelStr of it
= the RelStr of R & the mapping of it = (the carrier of it) --> p;
end;
registration
let R be RelStr, T be non empty 1-sorted, p be Element of T;
cluster ConstantNet(R,p) -> constant;
end;
registration
let R be non empty RelStr, T be non empty 1-sorted, p be Element of T;
cluster ConstantNet(R,p) -> non empty;
end;
registration
let R be non empty directed RelStr, T be non empty 1-sorted, p be Element of
T;
cluster ConstantNet(R,p) -> directed;
end;
registration
let R be non empty transitive RelStr, T be non empty 1-sorted, p be Element
of T;
cluster ConstantNet(R,p) -> transitive;
end;
theorem :: YELLOW_6:4
for R be RelStr, T be non empty 1-sorted, p be Element of T
holds the carrier of ConstantNet(R,p) = the carrier of R;
theorem :: YELLOW_6:5
for R be non empty RelStr, T be non empty 1-sorted, p be Element
of T, q be Element of ConstantNet(R,p) holds ConstantNet(R,p).q = p;
registration
let T be non empty 1-sorted, N be non empty NetStr over T;
cluster the mapping of N -> non empty;
end;
begin :: Substructures of Nets
theorem :: YELLOW_6:6
for R being RelStr holds R is full SubRelStr of R;
theorem :: YELLOW_6:7
for R being RelStr, S being SubRelStr of R, T being SubRelStr of
S holds T is SubRelStr of R;
definition
let S be 1-sorted, N be NetStr over S;
mode SubNetStr of N -> NetStr over S means
:: YELLOW_6:def 6
it is SubRelStr of N & the
mapping of it = (the mapping of N)|the carrier of it;
end;
theorem :: YELLOW_6:8
for S being 1-sorted, N being NetStr over S holds N is SubNetStr of N;
theorem :: YELLOW_6:9
for Q being 1-sorted, R being NetStr over Q, S being SubNetStr of R, T
being SubNetStr of S holds T is SubNetStr of R;
definition
let S be 1-sorted, N be NetStr over S, M be SubNetStr of N;
attr M is full means
:: YELLOW_6:def 7
M is full SubRelStr of N;
end;
registration
let S be 1-sorted, N be NetStr over S;
cluster full strict for SubNetStr of N;
end;
registration
let S be 1-sorted, N be non empty NetStr over S;
cluster full non empty strict for SubNetStr of N;
end;
theorem :: YELLOW_6:10
for S being 1-sorted, N being NetStr over S, M be SubNetStr of N
holds the carrier of M c= the carrier of N;
theorem :: YELLOW_6:11
for S being 1-sorted, N being NetStr over S, M be SubNetStr of N
, x,y being Element of N, i,j being Element of M st x = i & y = j & i <= j
holds x <= y;
theorem :: YELLOW_6:12
for S being 1-sorted, N being non empty NetStr over S, M be non
empty full SubNetStr of N, x,y being Element of N, i,j being Element of M st x
= i & y = j & x <= y holds i <= j;
begin :: More about Nets
registration
let T be non empty 1-sorted;
cluster constant strict for net of T;
end;
registration
let T be non empty 1-sorted, N be constant NetStr over T;
cluster the mapping of N -> constant;
end;
definition
let T be non empty 1-sorted, N be NetStr over T;
assume
N is constant non empty;
func the_value_of N -> Element of T equals
:: YELLOW_6:def 8
the_value_of the mapping
of N;
end;
theorem :: YELLOW_6:13
for R be non empty RelStr, T be non empty 1-sorted, p be Element
of T holds the_value_of (ConstantNet(R,p)) = p;
definition
let T be non empty 1-sorted, N be net of T;
mode subnet of N -> net of T means
:: YELLOW_6:def 9
ex f being Function of it, N st
the mapping of it = (the mapping of N)*f & for m being Element of N ex n being
Element of it st for p being Element of it st n <= p holds m <= f.p;
end;
theorem :: YELLOW_6:14
for T being non empty 1-sorted, N be net of T holds N is subnet of N;
theorem :: YELLOW_6:15
for T being non empty 1-sorted, N1,N2,N3 be net of T st N1 is subnet
of N2 & N2 is subnet of N3 holds N1 is subnet of N3;
theorem :: YELLOW_6:16
for T being non empty 1-sorted, N be constant net of T, i being
Element of N holds N.i = the_value_of N;
theorem :: YELLOW_6:17
for L being non empty 1-sorted, N being net of L, X,Y being set
st N is_eventually_in X & N is_eventually_in Y holds X meets Y;
theorem :: YELLOW_6:18
for S being non empty 1-sorted, N being net of S, M being subnet
of N, X st M is_often_in X holds N is_often_in X;
theorem :: YELLOW_6:19
for S being non empty 1-sorted, N being net of S, X st N
is_eventually_in X holds N is_often_in X;
theorem :: YELLOW_6:20
for S being non empty 1-sorted, N being net of S holds N
is_eventually_in the carrier of S;
begin :: The Restriction of a Net
definition
let S be 1-sorted, N be NetStr over S, X;
func N"X -> strict SubNetStr of N means
:: YELLOW_6:def 10
it is full SubRelStr of N & the carrier of it = (the mapping of N)"X;
end;
registration
let S be 1-sorted, N be transitive NetStr over S, X;
cluster N"X -> transitive full;
end;
theorem :: YELLOW_6:21
for S being non empty 1-sorted, N be net of S, X st N
is_often_in X holds N"X is non empty directed;
theorem :: YELLOW_6:22
for S being non empty 1-sorted, N being net of S, X st N
is_often_in X holds N"X is subnet of N;
theorem :: YELLOW_6:23
for S being non empty 1-sorted, N being net of S, X for M being
subnet of N st M = N"X holds M is_eventually_in X;
begin :: The Universe of Nets
definition
let X be non empty 1-sorted;
func NetUniv X -> set means
:: YELLOW_6:def 11
for x being object holds x in it iff ex N being strict net
of X st N = x & the carrier of N in the_universe_of the carrier of X;
end;
registration
let X be non empty 1-sorted;
cluster NetUniv X -> non empty;
end;
begin :: Parametrized Families of Nets, Iteration
definition
let X be set, T be 1-sorted;
mode net_set of X,T -> ManySortedSet of X means
:: YELLOW_6:def 12
for i being set st i in rng it holds i is net of T;
end;
theorem :: YELLOW_6:24
for X being set, T being 1-sorted, F being ManySortedSet of X
holds F is net_set of X,T iff for i being set st i in X holds F.i is net of T
;
definition
let X be non empty set, T be 1-sorted;
let J be net_set of X,T, i be Element of X;
redefine func J.i -> net of T;
end;
registration
let X be set, T be 1-sorted;
cluster -> RelStr-yielding for net_set of X,T;
end;
registration
let T be 1-sorted, Y be net of T;
cluster -> yielding_non-empty_carriers for net_set of the carrier of Y,T;
end;
registration
let T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y
,T;
cluster product J -> directed transitive;
end;
registration
let X be set, T be 1-sorted;
cluster -> yielding_non-empty_carriers for net_set of X,T;
end;
registration
let X be set, T be 1-sorted;
cluster yielding_non-empty_carriers for net_set of X,T;
end;
definition
let T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y
,T;
func Iterated J -> strict net of T means
:: YELLOW_6:def 13
the RelStr of it = [:Y,
product J:] & for i being Element of Y, f being Function st i in the carrier of
Y & f in the carrier of product J holds (the mapping of it).(i,f) =(the mapping
of J.i).(f.i);
end;
theorem :: YELLOW_6:25
for T being non empty 1-sorted, Y being net of T, J being
net_set of the carrier of Y,T st Y in NetUniv T & for i being Element of Y
holds J.i in NetUniv T holds Iterated J in NetUniv T;
theorem :: YELLOW_6:26
for T being non empty 1-sorted, N being net of T for J being
net_set of the carrier of N, T holds the carrier of Iterated J = [:the carrier
of N, product Carrier J:];
theorem :: YELLOW_6:27
for T being non empty 1-sorted, N being net of T, J being
net_set of the carrier of N, T, i being Element of N, f being Element of
product J, x being Element of Iterated J st x = [i,f] holds (Iterated J).x = (
the mapping of J.i).(f.i);
theorem :: YELLOW_6:28
for T being non empty 1-sorted, Y being net of T, J being
net_set of the carrier of Y,T holds rng the mapping of Iterated J c= union
the set of all
rng the mapping of J.i where i is Element of Y;
begin :: Poset of open neighborhoods
definition
let T be non empty TopSpace, p be Point of T;
func OpenNeighborhoods p -> RelStr equals
:: YELLOW_6:def 14
(InclPoset { V where V is Subset
of T: p in V & V is open })~;
end;
registration
let T be non empty TopSpace, p be Point of T;
cluster OpenNeighborhoods p -> non empty;
end;
theorem :: YELLOW_6:29
for T being non empty TopSpace, p being Point of T, x being
Element of OpenNeighborhoods p ex W being Subset of T st W = x & p in W & W is
open;
theorem :: YELLOW_6:30
for T be non empty TopSpace, p be Point of T for x being Subset
of T holds x in the carrier of OpenNeighborhoods p iff p in x & x is open;
theorem :: YELLOW_6:31
for T be non empty TopSpace, p be Point of T for x,y being
Element of OpenNeighborhoods p holds x <= y iff y c= x;
registration
let T be non empty TopSpace, p be Point of T;
cluster OpenNeighborhoods p -> transitive directed;
end;
begin :: Nets in topological spaces
definition
let T be non empty TopSpace, N be net of T;
func Lim N -> Subset of T means
:: YELLOW_6:def 15
for p being Point of T holds p in it
iff for V being a_neighborhood of p holds N is_eventually_in V;
end;
theorem :: YELLOW_6:32
for T being non empty TopSpace, N being net of T, Y being subnet
of N holds Lim N c= Lim Y;
theorem :: YELLOW_6:33
for T being non empty TopSpace, N be constant net of T holds
the_value_of N in Lim N;
theorem :: YELLOW_6:34
for T being non empty TopSpace, N be net of T, p be Point of T
st p in Lim N for d being Element of N ex S being Subset of T st S = { N.c
where c is Element of N : d <= c } & p in Cl S;
theorem :: YELLOW_6:35
for T being non empty TopSpace holds T is Hausdorff iff for N
being net of T, p,q being Point of T st p in Lim N & q in Lim N holds p = q;
registration
let T be Hausdorff non empty TopSpace, N be net of T;
cluster Lim N -> trivial;
end;
definition
let T be non empty TopSpace, N be net of T;
attr N is convergent means
:: YELLOW_6:def 16
Lim N <> {};
end;
registration
let T be non empty TopSpace;
cluster constant -> convergent for net of T;
end;
registration
let T be non empty TopSpace;
cluster convergent strict for net of T;
end;
definition
let T be Hausdorff non empty TopSpace, N be convergent net of T;
func lim N -> Element of T means
:: YELLOW_6:def 17
it in Lim N;
end;
theorem :: YELLOW_6:36
for T be Hausdorff non empty TopSpace, N be constant net of T holds
lim N = the_value_of N;
theorem :: YELLOW_6:37
for T being non empty TopSpace, N being net of T for p being Point of
T st not p in Lim N ex Y being subnet of N st not ex Z being subnet of Y st p
in Lim Z;
theorem :: YELLOW_6:38
for T being non empty TopSpace, N being net of T st N in NetUniv
T for p being Point of T st not p in Lim N ex Y being subnet of N st Y in
NetUniv T & not ex Z being subnet of Y st p in Lim Z;
theorem :: YELLOW_6:39
for T being non empty TopSpace, N being net of T, p being Point
of T st p in Lim N for J being net_set of the carrier of N, T st for i being
Element of N holds N.i in Lim(J.i) holds p in Lim Iterated J;
begin :: Convergence Classes
definition
let S be non empty 1-sorted;
mode Convergence-Class of S -> set means
:: YELLOW_6:def 18
it c= [:NetUniv S,the carrier of S :];
end;
registration
let S be non empty 1-sorted;
cluster -> Relation-like for Convergence-Class of S;
end;
definition
let T be non empty TopSpace;
func Convergence T -> Convergence-Class of T means
:: YELLOW_6:def 19
for N being net
of T, p being Point of T holds [N,p] in it iff N in NetUniv T & p in Lim N;
end;
definition
let T be non empty 1-sorted, C be Convergence-Class of T;
attr C is (CONSTANTS) means
:: YELLOW_6:def 20
for N being constant net of T st N in
NetUniv T holds [N,the_value_of N] in C;
attr C is (SUBNETS) means
:: YELLOW_6:def 21
for N being net of T, Y being subnet of N
st Y in NetUniv T for p being Element of T holds [N,p] in C implies [Y,p] in C;
attr C is (DIVERGENCE) means
:: YELLOW_6:def 22
for X being net of T, p being Element
of T st X in NetUniv T & not [X,p] in C ex Y being subnet of X st Y in NetUniv
T & not ex Z being subnet of Y st [Z,p] in C;
attr C is (ITERATED_LIMITS) means
:: YELLOW_6:def 23
for X being net of T, p being
Element of T st [X,p] in C for J being net_set of the carrier of X, T st for i
being Element of X holds [J.i,X.i] in C holds [Iterated J,p] in C;
end;
registration
let T be non empty TopSpace;
cluster Convergence T -> (CONSTANTS) (SUBNETS) (DIVERGENCE)
(ITERATED_LIMITS);
end;
definition
let S be non empty 1-sorted, C be Convergence-Class of S;
func ConvergenceSpace C -> strict TopStruct means
:: YELLOW_6:def 24
the carrier of it
= the carrier of S & the topology of it = { V where V is Subset of S: for p
being Element of S st p in V for N being net of S st [N,p] in C holds N
is_eventually_in V};
end;
registration
let S be non empty 1-sorted, C be Convergence-Class of S;
cluster ConvergenceSpace C -> non empty;
end;
registration
let S be non empty 1-sorted, C be Convergence-Class of S;
cluster ConvergenceSpace C -> TopSpace-like;
end;
theorem :: YELLOW_6:40
for S be non empty 1-sorted, C be Convergence-Class of S holds C
c= Convergence ConvergenceSpace C;
definition
let T be non empty 1-sorted, C be Convergence-Class of T;
attr C is topological means
:: YELLOW_6:def 25
C is (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS);
end;
registration
let T be non empty 1-sorted;
cluster non empty topological for Convergence-Class of T;
end;
registration
let T be non empty 1-sorted;
cluster topological -> (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS)
for Convergence-Class of T;
cluster (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) -> topological
for Convergence-Class of T;
end;
theorem :: YELLOW_6:41
for T being non empty 1-sorted, C being topological
Convergence-Class of T, S being Subset of (ConvergenceSpace C qua non empty
TopSpace) holds S is open iff for p being Element of T st p in S for N being
net of T st [N,p] in C holds N is_eventually_in S;
theorem :: YELLOW_6:42
for T being non empty 1-sorted, C being topological
Convergence-Class of T, S being Subset of (ConvergenceSpace C qua non empty
TopSpace) holds S is closed iff for p being Element of T holds for N being net
of T st [N,p] in C & N is_often_in S holds p in S;
theorem :: YELLOW_6:43
for T being non empty 1-sorted, C being topological
Convergence-Class of T, S being Subset of ConvergenceSpace C, p being Point of
ConvergenceSpace C st p in Cl S ex N being net of ConvergenceSpace C st [N,p]
in C & rng the mapping of N c= S & p in Lim N;
theorem :: YELLOW_6:44
for T be non empty 1-sorted, C be Convergence-Class of T holds
Convergence ConvergenceSpace C = C iff C is topological;