WAYBEL33: Compactness of Lim-inf Topology

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;

:: deftheorem defines lim_inf WAYBEL33:def 1 :

for L1, L2 being complete LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X1 being non empty Subset of L1
for X2 being non empty Subset of L2
for F1 being Filter of (BoolePoset X1)
for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2

proof end;

definition

let L be non empty TopRelStr ;

attr L is lim-inf means :Def2: :: WAYBEL33:def 2
the topology of L = xi L;

end;

:: deftheorem Def2 defines lim-inf WAYBEL33:def 2 :

registration

cluster non empty lim-inf -> non empty TopSpace-like for TopRelStr ;

coherence

proof end;

end;

theorem Th2: :: WAYBEL33:2

for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds
for N1 being NetStr over L1 ex N2 being strict NetStr over L2 st
( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )

proof end;

theorem Th3: :: WAYBEL33:3

for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds
for N1 being NetStr over L1 st N1 in NetUniv L1 holds
ex N2 being strict net of L2 st
( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )

proof end;

Lm1: now :: thesis:

let L1, L2 be non empty RelStr ; :: thesis:
let N1 be net of L1; :: thesis:
let N2 be net of L2; :: thesis:
assume that
A1: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and
A2: the mapping of N1 = the mapping of N2 ; :: thesis:
let j1 be Element of N1; :: thesis:
deffunc H₁( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ;
deffunc H₂( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ;
let j2 be Element of N2; :: thesis:
assume A3: j1 = j2 ; :: thesis:
thus H₂(j1) c= H₁(j2) :: thesis:

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in H₂(j1) ; :: thesis:
then consider i1 being Element of N1 such that
A4: y = N1 . i1 and
A5: i1 >= j1 ;
reconsider i1 = i1 as Element of N1 ;
reconsider i2 = i1, j2 = j2 as Element of N2 by A1;
A6: N1 . i1 = N2 . i2 by A2;
i2 >= j2 by A1, A3, A5, YELLOW_0:1;
hence y in H₁(j2) by A4, A6; :: thesis:

end;

Lm2: now :: thesis:

let L1, L2 be /\-complete Semilattice; :: thesis:
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis:
let N1 be net of L1; :: thesis:
let N2 be net of L2; :: thesis:
assume that
A2: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and
A3: the mapping of N1 = the mapping of N2 ; :: thesis:
deffunc H₁( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ;
deffunc H₂( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ;
set U1 = { ("/\" (H₂(j),L1)) where j is Element of N1 : verum } ;
set U2 = { ("/\" (H₁(j),L2)) where j is Element of N2 : verum } ;
thus { ("/\" (H₂(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H₁(j),L2)) where j is Element of N2 : verum } :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { ("/\" (H₂(j),L1)) where j is Element of N1 : verum } ; :: thesis:
then consider j1 being Element of N1 such that
A4: x = "/\" (H₂(j1),L1) ;
reconsider j2 = j1 as Element of N2 by A2;
( H₂(j1) c= H₁(j2) & H₁(j2) c= H₂(j1) ) by A2, A3, Lm1;
then A5: H₂(j1) = H₁(j2) ;
reconsider j1 = j1 as Element of N1 ;
A6: H₂(j1) c= the carrier of L1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in H₂(j1) ; :: thesis:
then ex i being Element of N1 st
( x = N1 . i & i >= j1 ) ;
hence x in the carrier of L1 ; :: thesis:

end;

[#] N1 is directed by WAYBEL_0:def 6;
then consider j0 being Element of N1 such that
j0 in the carrier of N1 and
A7: j1 <= j0 and
j1 <= j0 ;
N1 . j0 in H₂(j1) by A7;
then reconsider S = H₂(j1) as non empty Subset of L1 by A6;
ex_inf_of S,L1 by WAYBEL_0:76;
then x = "/\" (H₁(j2),L2) by A1, A4, A5, YELLOW_0:27;
hence x in { ("/\" (H₁(j),L2)) where j is Element of N2 : verum } ; :: thesis:

end;

theorem Th4: :: WAYBEL33:4

for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
lim_inf N1 = lim_inf N2

proof end;

theorem Th5: :: WAYBEL33:5

for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds
for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 )

proof end;

theorem Th6: :: WAYBEL33:6

for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for N1 being NetStr over L1
for a being set st [N1,a] in lim_inf-Convergence L1 holds
ex N2 being strict net of L2 st
( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )

proof end;

theorem Th7: :: 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 RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for X being set st N1 is_eventually_in X holds
N2 is_eventually_in X

proof end;

theorem :: WAYBEL33:8

for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2)

proof end;

theorem Th9: :: WAYBEL33:9

for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
xi L1 = xi L2

proof end;

registration

let R be non empty reflexive /\-complete RelStr ;

cluster -> /\-complete for TopAugmentation of R;

coherence

proof end;

end;

registration

let R be Semilattice;

cluster -> with_infima for TopAugmentation of R;

coherence

proof end;

end;

theorem Th10: :: WAYBEL33:10

for L being up-complete /\-complete Semilattice
for X being lim-inf TopAugmentation of L holds xi L = the topology of X

proof end;

definition

let L be up-complete /\-complete Semilattice;

func Xi L -> strict TopAugmentation of L means :Def3: :: WAYBEL33:def 3
it is lim-inf ;

uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def3 defines Xi WAYBEL33:def 3 :

registration

let L be up-complete /\-complete Semilattice;

cluster Xi L -> strict lim-inf ;

coherence by Def3;

end;

theorem Th11: :: WAYBEL33:11

for L being complete LATTICE
for N being net of L holds lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L)

proof end;

theorem Th12: :: WAYBEL33:12

for L being complete LATTICE
for F being proper Filter of (BoolePoset ([#] L))
for f being Subset of L st f in F holds
for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i)

proof end;

theorem Th13: :: WAYBEL33:13

for L being complete LATTICE
for F being proper Filter of (BoolePoset ([#] L)) holds lim_inf F = lim_inf (a_net F)

proof end;

theorem Th14: :: WAYBEL33:14

for L being complete LATTICE
for F being proper Filter of (BoolePoset ([#] L)) holds a_net F in NetUniv L

proof end;

theorem Th15: :: WAYBEL33:15

for L being complete LATTICE
for 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)

proof end;

theorem Th16: :: WAYBEL33:16

for L being complete LATTICE
for F being ultra Filter of (BoolePoset ([#] L))
for M being subnet of a_net F holds lim_inf F = lim_inf M

proof end;

theorem Th17: :: 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 holds
ex N9 being strict subnet of N st
( rng the mapping of N9 c= A & N9 is SubNetStr of N )

proof end;

theorem Th18: :: WAYBEL33:18

for L being complete lim-inf TopLattice
for 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 )

proof end;

theorem Th19: :: WAYBEL33:19

for L being non empty reflexive RelStr holds sigma L c= xi L by WAYBEL28:28;

theorem Th20: :: WAYBEL33:20

for T1, T2 being non empty TopSpace
for 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

proof end;

theorem Th21: :: WAYBEL33:21

for L being complete LATTICE holds omega L c= xi L

proof end;

theorem Th22: :: WAYBEL33:22

for T1, T2 being TopSpace
for T being non empty TopSpace st T is TopExtension of T1 & T is TopExtension of T2 holds
for R being Refinement of T1,T2 holds T is TopExtension of R

proof end;

theorem Th23: :: WAYBEL33:23

for T1 being TopSpace
for 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 ) )

proof end;

theorem Th24: :: WAYBEL33:24

for L being complete LATTICE holds lambda L c= xi L

proof end;

theorem Th25: :: WAYBEL33:25

for L being complete LATTICE
for T being lim-inf TopAugmentation of L
for S being correct Lawson TopAugmentation of L holds T is TopExtension of S

proof end;

theorem Th26: :: 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

proof end;

theorem :: WAYBEL33:27

for L being complete lim-inf TopLattice holds
( L is compact & L is T_1 )

proof end;