:: Compactness of Lim-inf Topology
:: by Grzegorz Bancerek and Noboru Endou
::
:: 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, ORDERS_2, SUBSET_1, CARD_FIL, YELLOW_1, ORDINAL2,
EQREL_1, REWRITE1, WAYBEL_0, TARSKI, STRUCT_0, ZFMISC_1, WAYBEL_9,
PRE_TOPC, WAYBEL28, YELLOW_6, SETFAM_1, FUNCT_1, XXREAL_0, LATTICES,
YELLOW_0, RELAT_1, RELAT_2, YELLOW_9, LATTICE3, YELLOW_2, YELLOW19,
MCART_1, CLASSES2, CLASSES1, METRIC_1, INT_2, RCOMP_1, FINSET_1, PROB_1,
CANTOR_1, RLVECT_3, ORDINAL1, PRELAMB, DIRAF, WAYBEL19, WAYBEL11,
WAYBEL_7, WAYBEL33, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1,
ORDERS_2, CARD_1, FINSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, LATTICE3, YELLOW_0,
CLASSES1, CLASSES2, CANTOR_1, WAYBEL_0, YELLOW_1, YELLOW_6, YELLOW_2,
WAYBEL_3, WAYBEL_7, WAYBEL_9, WAYBEL11, COMPTS_1, YELLOW_9, WAYBEL19,
WAYBEL28, YELLOW19;
constructors CLASSES1, TOLER_1, CLASSES2, REALSET2, CANTOR_1, WAYBEL_1,
WAYBEL_3, WAYBEL_7, WAYBEL11, YELLOW_9, WAYBEL19, WAYBEL28, YELLOW19,
COMPTS_1, RELSET_1, TOPS_2, WAYBEL_2, XTUPLE_0, XFAMILY;
registrations SUBSET_1, RELAT_1, FINSET_1, CLASSES2, STRUCT_0, TOPS_1,
LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_3, YELLOW_6, WAYBEL_7,
WAYBEL_9, YELLOW_9, WAYBEL19, YELLOW13, WAYBEL28, WAYBEL29, YELLOW19,
CARD_1, TEX_1, RELSET_1, XTUPLE_0;
requirements BOOLE, SUBSET;
begin
reserve x for set;
definition
let L be non empty Poset;
let X be non empty Subset of L;
let F be Filter of BoolePoset X;
func lim_inf F -> Element of L equals
:: WAYBEL33:def 1
"\/"({inf B where B is Subset of L: B
in F},L);
end;
theorem :: WAYBEL33:1
for L1, L2 being complete LATTICE st the RelStr of L1 = the RelStr of
L2 for X1 being non empty Subset of L1 for X2 being non empty Subset of L2 for
F1 being Filter of BoolePoset X1, F2 being Filter of BoolePoset X2 st F1 = F2
holds lim_inf F1 = lim_inf F2;
definition
let L be non empty TopRelStr;
attr L is lim-inf means
:: WAYBEL33:def 2
the topology of L = xi L;
end;
registration
cluster lim-inf -> TopSpace-like for non empty TopRelStr;
end;
registration
cluster trivial -> lim-inf for TopLattice;
end;
registration
cluster lim-inf continuous complete for TopLattice;
end;
theorem :: WAYBEL33:2
for L1, L2 being non empty 1-sorted st the carrier of L1 = the
carrier of L2 for N1 being NetStr over L1 ex N2 being strict NetStr over L2 st
the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2;
theorem :: WAYBEL33:3
for L1, L2 being non empty 1-sorted st the carrier of L1 = the
carrier of L2 for N1 being NetStr over L1 st N1 in NetUniv L1 ex N2 being
strict net of L2 st N2 in NetUniv L2 & the RelStr of N1 = the RelStr of N2 &
the mapping of N1 = the mapping of N2;
theorem :: WAYBEL33:4
for L1, L2 being /\-complete up-complete Semilattice st the
RelStr of L1 = the RelStr of L2 for N1 being net of L1, N2 being net of L2 st
the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2
holds lim_inf N1 = lim_inf N2;
theorem :: WAYBEL33:5
for L1, L2 being non empty 1-sorted st the carrier of L1 = the
carrier of L2 for N1 being net of L1, N2 being net of L2 st the RelStr of N1 =
the RelStr of N2 & the mapping of N1 = the mapping of N2 for S1 being subnet of
N1 ex S2 being strict subnet of N2 st the RelStr of S1 = the RelStr of S2 & the
mapping of S1 = the mapping of S2;
theorem :: WAYBEL33:6
for L1, L2 being /\-complete up-complete Semilattice st the
RelStr of L1 = the RelStr of L2 for N1 being NetStr over L1, a being set st [N1
,a] in lim_inf-Convergence L1 ex N2 being strict net of L2 st [N2,a] in
lim_inf-Convergence L2 & the RelStr of N1 = the RelStr of N2 & the mapping of
N1 = the mapping of N2;
theorem :: WAYBEL33:7
for L1, L2 being non empty 1-sorted for N1 being non empty NetStr
over L1 for N2 being non empty NetStr over L2 st the RelStr of N1 = the RelStr
of N2 & the mapping of N1 = the mapping of N2 for X being set st N1
is_eventually_in X holds N2 is_eventually_in X;
theorem :: WAYBEL33:8
for L1, L2 being /\-complete up-complete Semilattice st the RelStr of
L1 = the RelStr of L2 holds ConvergenceSpace lim_inf-Convergence L1 =
ConvergenceSpace lim_inf-Convergence L2;
theorem :: WAYBEL33:9
for L1, L2 being /\-complete up-complete Semilattice st the
RelStr of L1 = the RelStr of L2 holds xi L1 = xi L2;
registration
let R be /\-complete non empty reflexive RelStr;
cluster -> /\-complete for TopAugmentation of R;
end;
registration
let R be Semilattice;
cluster -> with_infima for TopAugmentation of R;
end;
registration
let L be /\-complete up-complete Semilattice;
cluster strict lim-inf for TopAugmentation of L;
end;
theorem :: WAYBEL33:10
for L being /\-complete up-complete Semilattice for X being
lim-inf TopAugmentation of L holds xi L = the topology of X;
definition
let L be /\-complete up-complete Semilattice;
func Xi L -> strict TopAugmentation of L means
:: WAYBEL33:def 3
it is lim-inf;
end;
registration
let L be /\-complete up-complete Semilattice;
cluster Xi L -> lim-inf;
end;
theorem :: WAYBEL33:11
for L being complete LATTICE, N being net of L holds lim_inf N =
"\/"((the set of all inf (N|i) where i is Element of N), L);
theorem :: WAYBEL33:12
for L being complete LATTICE, F being proper Filter of
BoolePoset [#]L, f being Subset of L st f in F for i being Element of a_net F
st i`2 = f holds inf f = inf ((a_net F)|i);
theorem :: WAYBEL33:13
for L being complete LATTICE, F being proper Filter of
BoolePoset [#]L holds lim_inf F = lim_inf a_net F;
theorem :: WAYBEL33:14
for L being complete LATTICE, F being proper Filter of
BoolePoset [#]L holds a_net F in NetUniv L;
theorem :: WAYBEL33:15
for L being complete LATTICE, F being ultra Filter of BoolePoset
[#]L for p being greater_or_equal_to_id Function of a_net F, a_net F holds
lim_inf F >= inf ((a_net F) * p);
theorem :: WAYBEL33:16
for L being complete LATTICE, F being ultra Filter of BoolePoset
[#]L holds for M being subnet of a_net F holds lim_inf F = lim_inf M;
theorem :: WAYBEL33:17
for L being non empty 1-sorted for N being net of L for A being
set st N is_often_in A ex N9 being strict subnet of N st rng the mapping of N9
c= A & N9 is SubNetStr of N;
theorem :: WAYBEL33:18 :: III. 3.4. LEMMA, p. 168(?)
for L being complete lim-inf TopLattice, A being non empty
Subset of L holds A is closed iff for F being ultra Filter of BoolePoset [#]L
st A in F holds lim_inf F in A;
theorem :: WAYBEL33:19
for L being non empty reflexive RelStr holds sigma L c= xi L;
theorem :: WAYBEL33:20
for T1, T2 being non empty TopSpace, B being prebasis of T1 st B
c= the topology of T2 & the carrier of T1 in the topology of T2 holds the
topology of T1 c= the topology of T2;
theorem :: WAYBEL33:21
for L being complete LATTICE holds omega L c= xi L;
theorem :: WAYBEL33:22
for T1,T2 being TopSpace, T being non empty TopSpace st T is
TopExtension of T1 & T is TopExtension of T2 for R being Refinement of T1,T2
holds T is TopExtension of R;
theorem :: WAYBEL33:23
for T1 being TopSpace, T2 being TopExtension of T1 for A being
Subset of T1 holds (A is open implies A is open Subset of T2) & (A is closed
implies A is closed Subset of T2);
theorem :: WAYBEL33:24 :: III. 3.5. LEMMA, p. 168(?)
for L being complete LATTICE holds lambda L c= xi L;
theorem :: WAYBEL33:25 :: 3.6. PROPOSITION (B), p. 169(?)
for L being complete LATTICE for T being lim-inf TopAugmentation
of L for S being Lawson correct TopAugmentation of L holds T is TopExtension of
S;
theorem :: WAYBEL33:26
for L being complete lim-inf TopLattice for F being ultra Filter
of BoolePoset [#]L holds lim_inf F is_a_convergence_point_of F, L;
::$N Compactness of Lim-inf Topology
theorem :: WAYBEL33:27 :: 3.6. PROPOSITION (A), p. 169(?)
for L being complete lim-inf TopLattice holds L is compact T_1;