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 X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2)
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 X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2)
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 X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2)
let Y be non empty Hausdorff regular TopSpace; for f being Function of [:X1,X2:],Y st ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2)
let f be Function of [:X1,X2:],Y; ( ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) implies lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2) )
assume A1:
for x1 being Element of X2 holds lim_filter ((ProjMap2 (f,x1)),cF1) <> {}
; lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2)
now for y0 being object st y0 in lim_filter (f,<.cF1,cF2.)) holds
y0 in lim_filter ((lim_in_cod1 (f,cF1)),cF2)let y0 be
object ;
( y0 in lim_filter (f,<.cF1,cF2.)) implies y0 in lim_filter ((lim_in_cod1 (f,cF1)),cF2) )assume A2:
y0 in lim_filter (
f,
<.cF1,cF2.))
;
y0 in lim_filter ((lim_in_cod1 (f,cF1)),cF2)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
B2 holds
lim_filter (
(ProjMap2 (f,z)),
cF1)
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 B2 holds lim_filter ((ProjMap2 (f,z)),cF1) 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 B2 holds lim_filter ((ProjMap2 (f,z)),cF1) c= Cl (Int U)
then consider B1 being
Element of
cB1,
B2 being
Element of
cB2 such that A6:
for
z being
Element of
X2 for
t being
Element of
Y st
z in B2 &
t in lim_filter (
(ProjMap2 (f,z)),
cF1) holds
t in Cl (Int U)
by A3, A4, A2, Th77;
take
B1
;
ex B2 being Element of cB2 st
for z being Element of B2 holds lim_filter ((ProjMap2 (f,z)),cF1) c= Cl (Int U)
take
B2
;
for z being Element of B2 holds lim_filter ((ProjMap2 (f,z)),cF1) c= Cl (Int U)
thus
for
z being
Element of
B2 holds
lim_filter (
(ProjMap2 (f,z)),
cF1)
c= Cl (Int U)
by A6;
verum
end;
NeighborhoodSystem y c= filter_image (
(lim_in_cod1 (f,cF1)),
cF2)
proof
let n be
object ;
TARSKI:def 3 ( not n in NeighborhoodSystem y or n in filter_image ((lim_in_cod1 (f,cF1)),cF2) )
assume
n in NeighborhoodSystem y
;
n in filter_image ((lim_in_cod1 (f,cF1)),cF2)
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
B2 holds
lim_filter (
(ProjMap2 (f,z)),
cF1)
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 ( B2 c= (lim_in_cod1 (f,cF1)) " n1 & (lim_in_cod1 (f,cF1)) " n1 is Subset of X2 )
(lim_in_cod1 (f,cF1)) .: B2 c= n1
proof
let t be
object ;
TARSKI:def 3 ( not t in (lim_in_cod1 (f,cF1)) .: B2 or t in n1 )
assume
t in (lim_in_cod1 (f,cF1)) .: B2
;
t in n1
then consider u being
object such that A14:
u in dom (lim_in_cod1 (f,cF1))
and A15:
u in B2
and A16:
t = (lim_in_cod1 (f,cF1)) . u
by FUNCT_1:def 6;
reconsider u1 =
u as
Element of
X2 by A14;
{t} = lim_filter (
(ProjMap2 (f,u1)),
cF1)
by A16, A1, Def6;
then A17:
t in lim_filter (
(ProjMap2 (f,u1)),
cF1)
by TARSKI:def 1;
lim_filter (
(ProjMap2 (f,u1)),
cF1)
c= Cl (Int Q)
by A11, A15;
hence
t in n1
by A7, A17, A13, A12, A9;
verum
end; hence
B2 c= (lim_in_cod1 (f,cF1)) " n1
by FUNCT_2:95;
(lim_in_cod1 (f,cF1)) " n1 is Subset of X2
dom (lim_in_cod1 (f,cF1)) = X2
by FUNCT_2:def 1;
hence
(lim_in_cod1 (f,cF1)) " n1 is
Subset of
X2
by RELAT_1:132;
verum end;
then
(lim_in_cod1 (f,cF1)) " n1 in cF2
by A4, CARDFIL2:def 8;
hence
n in filter_image (
(lim_in_cod1 (f,cF1)),
cF2)
;
verum
end; then
filter_image (
(lim_in_cod1 (f,cF1)),
cF2)
is_filter-finer_than NeighborhoodSystem y
;
hence
y0 in lim_filter (
(lim_in_cod1 (f,cF1)),
cF2)
;
verum end;
hence
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2)
; verum