let T be LinearTopSpace; :: thesis: for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of T
for x being Point of T
for V being local_base of T st [#] L is directed holds
( x in lim_f f iff for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds
ex i being Element of L st
for j being Element of L st i <= j holds
f . j in x + v )
let L be non empty reflexive transitive RelStr ; :: thesis: for f being Function of ([#] L), the carrier of T
for x being Point of T
for V being local_base of T st [#] L is directed holds
( x in lim_f f iff for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds
ex i being Element of L st
for j being Element of L st i <= j holds
f . j in x + v )
let f be Function of ([#] L), the carrier of T; :: thesis: for x being Point of T
for V being local_base of T st [#] L is directed holds
( x in lim_f f iff for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds
ex i being Element of L st
for j being Element of L st i <= j holds
f . j in x + v )
let x be Point of T; :: thesis: for V being local_base of T st [#] L is directed holds
( x in lim_f f iff for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds
ex i being Element of L st
for j being Element of L st i <= j holds
f . j in x + v )
let V be local_base of T; :: thesis: ( [#] L is directed implies ( x in lim_f f iff for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds
ex i being Element of L st
for j being Element of L st i <= j holds
f . j in x + v ) )
assume A1: [#] L is directed ; :: thesis: ( x in lim_f f iff for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds
ex i being Element of L st
for j being Element of L st i <= j holds
f . j in x + v )
set B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } ;
reconsider B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } as Subset-Family of T by Lm2;
now :: thesis: ( ( x in lim_f f implies for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds
ex i0 being Element of L st
for j being Element of L st i0 <= j holds
f . j in x + v ) & ( ( for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds
ex i being Element of L st
for j being Element of L st i <= j holds
f . j in x + v ) implies x in lim_f f ) )
hereby :: thesis: ( ( for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds
ex i being Element of L st
for j being Element of L st i <= j holds
f . j in x + v ) implies x in lim_f f )
assume A2: x in lim_f f ; :: thesis: for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds
ex i0 being Element of L st
for j being Element of L st i0 <= j holds
f . j in x + v
let v be Subset of T; :: thesis: ( v in V /\ (NeighborhoodSystem (0. T)) implies ex i0 being Element of L st
for j being Element of L st i0 <= j holds
f . j in x + v )
assume v in V /\ (NeighborhoodSystem (0. T)) ; :: thesis: ex i0 being Element of L st
for j being Element of L st i0 <= j holds
f . j in x + v
then ( v in V & v in NeighborhoodSystem (0. T) ) by XBOOLE_0:def 4;
then ( v in V & v is a_neighborhood of 0. T ) by YELLOW19:2;
then x + v in B ;
then reconsider b = x + v as Element of B ;
consider i0 being Element of L such that
A3: for j being Element of L st i0 <= j holds
f . j in b by A1, A2, Lm3;
take i0 = i0; :: thesis: for j being Element of L st i0 <= j holds
f . j in x + v
thus for j being Element of L st i0 <= j holds
f . j in x + v by A3; :: thesis: verum
end;
assume A4: for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds
ex i being Element of L st
for j being Element of L st i <= j holds
f . j in x + v ; :: thesis: x in lim_f f
for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b
proof
let b be Element of B; :: thesis: ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b
not B is empty by Lm2;
then b in B ;
then consider U1 being Subset of T such that
A5: b = x + U1 and
A6: U1 in V and
A7: U1 is a_neighborhood of 0. T ;
U1 in NeighborhoodSystem (0. T) by A7, YELLOW19:2;
then U1 in V /\ (NeighborhoodSystem (0. T)) by A6, XBOOLE_0:def 4;
then consider i0 being Element of L such that
A8: for j being Element of L st i0 <= j holds
f . j in x + U1 by A4;
take i0 ; :: thesis: for j being Element of L st i0 <= j holds
f . j in b
thus for j being Element of L st i0 <= j holds
f . j in b by A5, A8; :: thesis: verum
end;
hence x in lim_f f by A1, Lm3; :: thesis: verum
end;
hence ( x in lim_f f iff for v being Subset of T st v in V /\ (NeighborhoodSystem (0. T)) holds
ex i being Element of L st
for j being Element of L st i <= j holds
f . j in x + v ) ; :: thesis: verum