let X1, X2 be non empty set ; for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty Hausdorff regular TopSpace
for f being Function of [:X1,X2:],Y st ( for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1)
let cF1 be Filter of X1; for cF2 being Filter of X2
for Y being non empty Hausdorff regular TopSpace
for f being Function of [:X1,X2:],Y st ( for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1)
let cF2 be Filter of X2; for Y being non empty Hausdorff regular TopSpace
for f being Function of [:X1,X2:],Y st ( for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1)
let Y be non empty Hausdorff regular TopSpace; for f being Function of [:X1,X2:],Y st ( for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1)
let f be Function of [:X1,X2:],Y; ( ( for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) implies lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1) )
assume A1:
for x1 being Element of X1 holds lim_filter ((ProjMap1 (f,x1)),cF2) <> {}
; lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1)
now for y0 being object st y0 in lim_filter (f,<.cF1,cF2.)) holds
y0 in lim_filter ((lim_in_cod2 (f,cF2)),cF1)let y0 be
object ;
( y0 in lim_filter (f,<.cF1,cF2.)) implies y0 in lim_filter ((lim_in_cod2 (f,cF2)),cF1) )assume A2:
y0 in lim_filter (
f,
<.cF1,cF2.))
;
y0 in lim_filter ((lim_in_cod2 (f,cF2)),cF1)then reconsider y =
y0 as
Element of
Y ;
consider cB1 being
filter_base of
X1 such that
cB1 = cF1
and A3:
<.cB1.) = cF1
by Th18;
consider cB2 being
filter_base of
X2 such that
cB2 = cF2
and A4:
<.cB2.) = cF2
by Th18;
A5:
for
U being
a_neighborhood of
y st
U is
closed holds
ex
B1 being
Element of
cB1 ex
B2 being
Element of
cB2 st
for
z being
Element of
B1 holds
lim_filter (
(ProjMap1 (f,z)),
cF2)
c= Cl (Int U)
proof
let U be
a_neighborhood of
y;
( U is closed implies ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of B1 holds lim_filter ((ProjMap1 (f,z)),cF2) c= Cl (Int U) )
assume
U is
closed
;
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of B1 holds lim_filter ((ProjMap1 (f,z)),cF2) c= Cl (Int U)
then consider B1 being
Element of
cB1,
B2 being
Element of
cB2 such that A6:
for
z being
Element of
X1 for
t being
Element of
Y st
z in B1 &
t in lim_filter (
(ProjMap1 (f,z)),
cF2) holds
t in Cl (Int U)
by A3, A4, A2, Th76;
take
B1
;
ex B2 being Element of cB2 st
for z being Element of B1 holds lim_filter ((ProjMap1 (f,z)),cF2) c= Cl (Int U)
take
B2
;
for z being Element of B1 holds lim_filter ((ProjMap1 (f,z)),cF2) c= Cl (Int U)
thus
for
z being
Element of
B1 holds
lim_filter (
(ProjMap1 (f,z)),
cF2)
c= Cl (Int U)
by A6;
verum
end;
NeighborhoodSystem y c= filter_image (
(lim_in_cod2 (f,cF2)),
cF1)
proof
let n be
object ;
TARSKI:def 3 ( not n in NeighborhoodSystem y or n in filter_image ((lim_in_cod2 (f,cF2)),cF1) )
assume
n in NeighborhoodSystem y
;
n in filter_image ((lim_in_cod2 (f,cF2)),cF1)
then
n in { A where A is a_neighborhood of y : verum }
by YELLOW19:def 1;
then consider A being
a_neighborhood of
y such that A7:
n = A
;
y in Int A
by CONNSP_2:def 1;
then consider Q being
Subset of
Y such that A8:
Q is
closed
and A9:
Q c= A
and A10:
y in Int Q
by YELLOW_8:27;
Q is
a_neighborhood of
y
by A10, CONNSP_2:def 1;
then consider B1 being
Element of
cB1,
B2 being
Element of
cB2 such that A11:
for
z being
Element of
B1 holds
lim_filter (
(ProjMap1 (f,z)),
cF2)
c= Cl (Int Q)
by A8, A5;
A12:
Cl Q = Q
by PRE_TOPC:18, A8, TOPS_1:5;
A13:
Cl (Int Q) c= Cl Q
by TOPS_1:16, PRE_TOPC:19;
reconsider n1 =
n as
Subset of
Y by A7;
now ( B1 c= (lim_in_cod2 (f,cF2)) " n1 & (lim_in_cod2 (f,cF2)) " n1 is Subset of X1 )
(lim_in_cod2 (f,cF2)) .: B1 c= n1
proof
let t be
object ;
TARSKI:def 3 ( not t in (lim_in_cod2 (f,cF2)) .: B1 or t in n1 )
assume
t in (lim_in_cod2 (f,cF2)) .: B1
;
t in n1
then consider u being
object such that A14:
u in dom (lim_in_cod2 (f,cF2))
and A15:
u in B1
and A16:
t = (lim_in_cod2 (f,cF2)) . u
by FUNCT_1:def 6;
reconsider u1 =
u as
Element of
X1 by A14;
{t} = lim_filter (
(ProjMap1 (f,u1)),
cF2)
by A16, A1, Def7;
then A17:
t in lim_filter (
(ProjMap1 (f,u1)),
cF2)
by TARSKI:def 1;
lim_filter (
(ProjMap1 (f,u1)),
cF2)
c= Cl (Int Q)
by A11, A15;
hence
t in n1
by A7, A17, A13, A12, A9;
verum
end; hence
B1 c= (lim_in_cod2 (f,cF2)) " n1
by FUNCT_2:95;
(lim_in_cod2 (f,cF2)) " n1 is Subset of X1
dom (lim_in_cod2 (f,cF2)) = X1
by FUNCT_2:def 1;
hence
(lim_in_cod2 (f,cF2)) " n1 is
Subset of
X1
by RELAT_1:132;
verum end;
then
(lim_in_cod2 (f,cF2)) " n1 in cF1
by A3, CARDFIL2:def 8;
hence
n in filter_image (
(lim_in_cod2 (f,cF2)),
cF1)
;
verum
end; then
filter_image (
(lim_in_cod2 (f,cF2)),
cF1)
is_filter-finer_than NeighborhoodSystem y
;
hence
y0 in lim_filter (
(lim_in_cod2 (f,cF2)),
cF1)
;
verum end;
hence
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1)
; verum