:: On the characterizations of compactness
:: by Grzegorz Bancerek , Noboru Endou and Yuji Sakai
::
:: Received July 29, 2001
:: Copyright (c) 2001-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 XBOOLE_0, SUBSET_1, CARD_FIL, YELLOW_1, LATTICES, PRE_TOPC,
CONNSP_2, STRUCT_0, TARSKI, ZFMISC_1, WAYBEL_0, XXREAL_0, TOPS_1,
WAYBEL_7, RCOMP_1, RELAT_1, RELAT_2, FUNCT_1, FINSET_1, SETFAM_1,
LATTICE3, ORDERS_2, WELLORD2, ORDINAL1, MCART_1, YELLOW_6, SEQ_2,
METRIC_1, CANTOR_1, ARYTM_0, ARYTM_3, CLASSES1, INT_2, YELLOW_0, CAT_1,
BHSP_3, YELLOW19;
notations TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, RELAT_1, MCART_1,
SETFAM_1, FINSET_1, FUNCT_1, RELAT_2, RELSET_1, PARTFUN1, FUNCT_2,
CLASSES1, ORDERS_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1,
CONNSP_2, CANTOR_1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1,
WAYBEL_7, YELLOW_6, WAYBEL_9, YELLOW_7, WAYBEL32;
constructors CLASSES1, TOLER_1, TOPS_1, TOPS_2, CONNSP_2, CANTOR_1, WAYBEL_1,
WAYBEL_7, WAYBEL32, COMPTS_1, RELSET_1, XTUPLE_0, XFAMILY;
registrations SUBSET_1, RELAT_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_1,
LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_6, WAYBEL_7, WAYBEL_9,
WAYBEL32, RELSET_1, XTUPLE_0;
requirements BOOLE, SUBSET;
begin
reserve x,y,X for set;
theorem :: YELLOW19:1
for X being non empty set for F being proper Filter of BoolePoset
X for A being set st A in F holds A is not empty;
definition
let T be non empty TopSpace;
let x be Point of T;
func NeighborhoodSystem x -> Subset of BoolePoset [#]T equals
:: YELLOW19:def 1
the set of all A where A is
a_neighborhood of x;
end;
theorem :: YELLOW19:2
for T being non empty TopSpace, x being Point of T, A being set
holds A in NeighborhoodSystem x iff A is a_neighborhood of x;
registration
let T be non empty TopSpace;
let x be Point of T;
cluster NeighborhoodSystem x -> non empty proper upper filtered;
end;
theorem :: YELLOW19:3
for T being non empty TopSpace, x being Point of T for F being
upper Subset of BoolePoset [#]T holds x is_a_convergence_point_of F, T iff
NeighborhoodSystem x c= F;
theorem :: YELLOW19:4
for T being non empty TopSpace, x being Point of T holds x
is_a_convergence_point_of NeighborhoodSystem x, T;
theorem :: YELLOW19:5
for T being non empty TopSpace for A being Subset of T holds A is open
iff for x being Point of T st x in A for F being Filter of BoolePoset [#]T st x
is_a_convergence_point_of F, T holds A in F;
definition
let S be non empty 1-sorted;
let N be non empty NetStr over S;
mode Subset of S,N -> Subset of S means
:: YELLOW19:def 2
ex i being Element of N st it = rng the mapping of N|i;
end;
theorem :: YELLOW19:6
for S being non empty 1-sorted for N being non empty NetStr over S for
i being Element of N holds rng the mapping of N|i is Subset of S, N;
registration
let S be non empty 1-sorted;
let N be reflexive non empty NetStr over S;
cluster -> non empty for Subset of S,N;
end;
theorem :: YELLOW19:7
for S being non empty 1-sorted, N being net of S for i being
Element of N, x being set holds x in rng the mapping of N|i iff ex j being
Element of N st i <= j & x = N.j;
theorem :: YELLOW19:8
for S being non empty 1-sorted, N being net of S for A being
Subset of S,N holds N is_eventually_in A;
theorem :: YELLOW19:9
for S being non empty 1-sorted, N being net of S for F being finite
non empty set st for A being Element of F holds A is Subset of S,N ex B being
Subset of S,N st B c= meet F;
definition
let T be non empty 1-sorted;
let N be non empty NetStr over T;
func a_filter N -> Subset of BoolePoset [#]T equals
:: YELLOW19:def 3
{A where A is Subset of
T: N is_eventually_in A};
end;
theorem :: YELLOW19:10
for T being non empty 1-sorted for N being non empty NetStr over
T for A being set holds A in a_filter N iff N is_eventually_in A & A is Subset
of T;
registration
let T be non empty 1-sorted;
let N be non empty NetStr over T;
cluster a_filter N -> non empty upper;
end;
registration
let T be non empty 1-sorted;
let N be net of T;
cluster a_filter N -> proper filtered;
end;
theorem :: YELLOW19:11
for T being non empty TopSpace for N being net of T for x being
Point of T holds x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter
N, T;
theorem :: YELLOW19:12
for T being non empty TopSpace for N being net of T for x being
Point of T holds x in Lim N iff x is_a_convergence_point_of a_filter N, T;
definition
let L be non empty 1-sorted;
let O be non empty Subset of L;
let F be Filter of BoolePoset O;
func a_net F -> strict non empty NetStr over L means
:: YELLOW19:def 4
the carrier of
it = {[a, f] where a is Element of L, f is Element of F: a in f} & (for i,j
being Element of it holds i <= j iff j`2 c= i`2) & for i being Element of it
holds it.i = i`1;
end;
registration
let L be non empty 1-sorted;
let O be non empty Subset of L;
let F be Filter of BoolePoset O;
cluster a_net F -> reflexive transitive;
end;
registration
let L be non empty 1-sorted;
let O be non empty Subset of L;
let F be proper Filter of BoolePoset O;
cluster a_net F -> directed;
end;
theorem :: YELLOW19:13
for T being non empty 1-sorted for F being Filter of BoolePoset
[#]T holds F \ {{}} = a_filter a_net F;
theorem :: YELLOW19:14
for T being non empty 1-sorted for F being proper Filter of
BoolePoset [#]T holds F = a_filter a_net F;
theorem :: YELLOW19:15
for T being non empty 1-sorted for F being Filter of BoolePoset
[#]T for A being non empty Subset of T holds A in F iff a_net F
is_eventually_in A;
theorem :: YELLOW19:16
for T being non empty TopSpace for F being proper Filter of
BoolePoset [#]T for x being Point of T holds x is_a_cluster_point_of a_net F
iff x is_a_cluster_point_of F, T;
theorem :: YELLOW19:17
for T being non empty TopSpace for F being proper Filter of
BoolePoset [#]T for x being Point of T holds x in Lim a_net F iff x
is_a_convergence_point_of F, T;
theorem :: YELLOW19:18
for T being non empty TopSpace, x being Point of T, A being
Subset of T st x in Cl A for F being proper Filter of BoolePoset [#]T st F =
NeighborhoodSystem x holds a_net F is_often_in A;
theorem :: YELLOW19:19
for T being non empty 1-sorted, A being set for N being net of T
st N is_eventually_in A for S being subnet of N holds S is_eventually_in A;
theorem :: YELLOW19:20
for T being non empty TopSpace, F,G,x being set st F c= G & x
is_a_convergence_point_of F, T holds x is_a_convergence_point_of G, T;
theorem :: YELLOW19:21
for T being non empty TopSpace, A being Subset of T for x being
Point of T holds x in Cl A iff ex N being net of T st N is_eventually_in A & x
is_a_cluster_point_of N;
theorem :: YELLOW19:22
for T being non empty TopSpace, A being Subset of T for x being
Point of T holds x in Cl A iff ex N being convergent net of T st N
is_eventually_in A & x in Lim N;
theorem :: YELLOW19:23
for T being non empty TopSpace, A being Subset of T holds A is closed
iff for N being net of T st N is_eventually_in A for x being Point of T st x
is_a_cluster_point_of N holds x in A;
theorem :: YELLOW19:24
for T being non empty TopSpace, A being Subset of T holds A is closed
iff for N being convergent net of T st N is_eventually_in A for x being Point
of T st x in Lim N holds x in A;
theorem :: YELLOW19:25
for T being non empty TopSpace, A being Subset of T for x being
Point of T holds x in Cl A iff ex F being proper Filter of BoolePoset [#]T st A
in F & x is_a_cluster_point_of F, T;
theorem :: YELLOW19:26
for T being non empty TopSpace, A being Subset of T for x being
Point of T holds x in Cl A iff ex F being ultra Filter of BoolePoset [#]T st A
in F & x is_a_convergence_point_of F, T;
theorem :: YELLOW19:27
for T being non empty TopSpace, A being Subset of T holds A is closed
iff for F being proper Filter of BoolePoset [#]T st A in F for x being Point of
T st x is_a_cluster_point_of F,T holds x in A;
theorem :: YELLOW19:28
for T being non empty TopSpace, A being Subset of T holds A is closed
iff for F being ultra Filter of BoolePoset [#]T st A in F for x being Point of
T st x is_a_convergence_point_of F,T holds x in A;
theorem :: YELLOW19:29
for T being non empty TopSpace, N being net of T for s being
Point of T holds s is_a_cluster_point_of N iff for A being Subset of T,N holds
s in Cl A;
theorem :: YELLOW19:30
for T being non empty TopSpace for F being Subset-Family of T st F is
closed holds FinMeetCl F is closed;
theorem :: YELLOW19:31
for T being non empty TopSpace holds T is compact iff for F
being ultra Filter of BoolePoset [#]T ex x being Point of T st x
is_a_convergence_point_of F, T;
theorem :: YELLOW19:32
for T being non empty TopSpace holds T is compact iff for F being
proper Filter of BoolePoset [#]T ex x being Point of T st x
is_a_cluster_point_of F, T;
theorem :: YELLOW19:33
for T being non empty TopSpace holds T is compact iff for N
being net of T ex x being Point of T st x is_a_cluster_point_of N;
theorem :: YELLOW19:34
for T being non empty TopSpace holds T is compact iff for N being net
of T st N in NetUniv T ex x being Point of T st x is_a_cluster_point_of N;
registration
let L be non empty 1-sorted;
let N be transitive NetStr over L;
cluster -> transitive for full SubNetStr of N;
end;
registration
let L be non empty 1-sorted;
let N be non empty directed NetStr over L;
cluster strict non empty directed full for SubNetStr of N;
end;
theorem :: YELLOW19:35
for T being non empty TopSpace holds T is compact iff for N being net
of T ex S being subnet of N st S is convergent;
definition
let S be non empty 1-sorted;
let N be non empty NetStr over S;
attr N is Cauchy means
:: YELLOW19:def 5
for A being Subset of S holds N is_eventually_in A or N is_eventually_in A `;
end;
registration
let S be non empty 1-sorted;
let F be ultra Filter of BoolePoset [#]S;
cluster a_net F -> Cauchy;
end;
theorem :: YELLOW19:36
for T being non empty TopSpace holds T is compact iff for N being net
of T st N is Cauchy holds N is convergent;