Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-homlim Unicode version

Definition df-homlim 23984
Description: The input to this function is a sequence (on  NN) of structures  R ( n ) and homomorphisms  F ( n ) : R ( n ) --> R ( n  +  1 ). The resulting structure is the direct limit of the direct system so defined, and maintains any structures that were present in the original objects. TODO: generalize to directed sets? (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-homlim  |- HomLim  =  ( r  e.  _V , 
f  e.  _V  |->  [_ ( HomLimB  `  f )  / 
e ]_ [_ ( 1st `  e )  /  v ]_ [_ ( 2nd `  e
)  /  g ]_ ( { <. ( Base `  ndx ) ,  v >. , 
<. ( +g  `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( g `
 n ) ,  y  e.  dom  (
g `  n )  |-> 
<. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( ( g `
 n ) `  ( x ( +g  `  ( r `  n
) ) y ) ) >. ) >. ,  <. ( .r `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( .r `  (
r `  n )
) y ) )
>. ) >. }  u.  { <. ( TopOpen `  ndx ) ,  { s  e.  ~P v  |  A. n  e.  NN  ( `' ( g `  n )
" s )  e.  ( TopOpen `  ( r `  n ) ) }
>. ,  <. ( dist `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( ( g `  n ) `  n
) ,  y  e. 
dom  ( ( g `
 n ) `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( x ( dist `  (
r `  n )
) y ) >.
) >. ,  <. ( le `  ndx ) , 
U_ n  e.  NN  ( `' ( g `  n )  o.  (
( le `  (
r `  n )
)  o.  ( g `
 n ) ) ) >. } ) )
Distinct variable group:    e, f, g, n, r, s, v, x, y

Detailed syntax breakdown of Definition df-homlim
StepHypRef Expression
1 chlim 23976 . 2  class HomLim
2 vr . . 3  set  r
3 vf . . 3  set  f
4 cvv 2801 . . 3  class  _V
5 ve . . . 4  set  e
63cv 1631 . . . . 5  class  f
7 chlb 23975 . . . . 5  class HomLimB
86, 7cfv 5271 . . . 4  class  ( HomLimB  `  f
)
9 vv . . . . 5  set  v
105cv 1631 . . . . . 6  class  e
11 c1st 6136 . . . . . 6  class  1st
1210, 11cfv 5271 . . . . 5  class  ( 1st `  e )
13 vg . . . . . 6  set  g
14 c2nd 6137 . . . . . . 7  class  2nd
1510, 14cfv 5271 . . . . . 6  class  ( 2nd `  e )
16 cnx 13161 . . . . . . . . . 10  class  ndx
17 cbs 13164 . . . . . . . . . 10  class  Base
1816, 17cfv 5271 . . . . . . . . 9  class  ( Base `  ndx )
199cv 1631 . . . . . . . . 9  class  v
2018, 19cop 3656 . . . . . . . 8  class  <. ( Base `  ndx ) ,  v >.
21 cplusg 13224 . . . . . . . . . 10  class  +g
2216, 21cfv 5271 . . . . . . . . 9  class  ( +g  ` 
ndx )
23 vn . . . . . . . . . 10  set  n
24 cn 9762 . . . . . . . . . 10  class  NN
25 vx . . . . . . . . . . . 12  set  x
26 vy . . . . . . . . . . . 12  set  y
2723cv 1631 . . . . . . . . . . . . . 14  class  n
2813cv 1631 . . . . . . . . . . . . . 14  class  g
2927, 28cfv 5271 . . . . . . . . . . . . 13  class  ( g `
 n )
3029cdm 4705 . . . . . . . . . . . 12  class  dom  (
g `  n )
3125cv 1631 . . . . . . . . . . . . . . 15  class  x
3231, 29cfv 5271 . . . . . . . . . . . . . 14  class  ( ( g `  n ) `
 x )
3326cv 1631 . . . . . . . . . . . . . . 15  class  y
3433, 29cfv 5271 . . . . . . . . . . . . . 14  class  ( ( g `  n ) `
 y )
3532, 34cop 3656 . . . . . . . . . . . . 13  class  <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >.
362cv 1631 . . . . . . . . . . . . . . . . 17  class  r
3727, 36cfv 5271 . . . . . . . . . . . . . . . 16  class  ( r `
 n )
3837, 21cfv 5271 . . . . . . . . . . . . . . 15  class  ( +g  `  ( r `  n
) )
3931, 33, 38co 5874 . . . . . . . . . . . . . 14  class  ( x ( +g  `  (
r `  n )
) y )
4039, 29cfv 5271 . . . . . . . . . . . . 13  class  ( ( g `  n ) `
 ( x ( +g  `  ( r `
 n ) ) y ) )
4135, 40cop 3656 . . . . . . . . . . . 12  class  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( +g  `  ( r `
 n ) ) y ) ) >.
4225, 26, 30, 30, 41cmpt2 5876 . . . . . . . . . . 11  class  ( x  e.  dom  ( g `
 n ) ,  y  e.  dom  (
g `  n )  |-> 
<. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( ( g `
 n ) `  ( x ( +g  `  ( r `  n
) ) y ) ) >. )
4342crn 4706 . . . . . . . . . 10  class  ran  (
x  e.  dom  (
g `  n ) ,  y  e.  dom  ( g `  n
)  |->  <. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( ( g `
 n ) `  ( x ( +g  `  ( r `  n
) ) y ) ) >. )
4423, 24, 43ciun 3921 . . . . . . . . 9  class  U_ n  e.  NN  ran  ( x  e.  dom  ( g `
 n ) ,  y  e.  dom  (
g `  n )  |-> 
<. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( ( g `
 n ) `  ( x ( +g  `  ( r `  n
) ) y ) ) >. )
4522, 44cop 3656 . . . . . . . 8  class  <. ( +g  `  ndx ) , 
U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( +g  `  ( r `
 n ) ) y ) ) >.
) >.
46 cmulr 13225 . . . . . . . . . 10  class  .r
4716, 46cfv 5271 . . . . . . . . 9  class  ( .r
`  ndx )
4837, 46cfv 5271 . . . . . . . . . . . . . . 15  class  ( .r
`  ( r `  n ) )
4931, 33, 48co 5874 . . . . . . . . . . . . . 14  class  ( x ( .r `  (
r `  n )
) y )
5049, 29cfv 5271 . . . . . . . . . . . . 13  class  ( ( g `  n ) `
 ( x ( .r `  ( r `
 n ) ) y ) )
5135, 50cop 3656 . . . . . . . . . . . 12  class  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( .r `  (
r `  n )
) y ) )
>.
5225, 26, 30, 30, 51cmpt2 5876 . . . . . . . . . . 11  class  ( x  e.  dom  ( g `
 n ) ,  y  e.  dom  (
g `  n )  |-> 
<. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( ( g `
 n ) `  ( x ( .r
`  ( r `  n ) ) y ) ) >. )
5352crn 4706 . . . . . . . . . 10  class  ran  (
x  e.  dom  (
g `  n ) ,  y  e.  dom  ( g `  n
)  |->  <. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( ( g `
 n ) `  ( x ( .r
`  ( r `  n ) ) y ) ) >. )
5423, 24, 53ciun 3921 . . . . . . . . 9  class  U_ n  e.  NN  ran  ( x  e.  dom  ( g `
 n ) ,  y  e.  dom  (
g `  n )  |-> 
<. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( ( g `
 n ) `  ( x ( .r
`  ( r `  n ) ) y ) ) >. )
5547, 54cop 3656 . . . . . . . 8  class  <. ( .r `  ndx ) , 
U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( .r `  (
r `  n )
) y ) )
>. ) >.
5620, 45, 55ctp 3655 . . . . . . 7  class  { <. (
Base `  ndx ) ,  v >. ,  <. ( +g  `  ndx ) , 
U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( +g  `  ( r `
 n ) ) y ) ) >.
) >. ,  <. ( .r `  ndx ) , 
U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( .r `  (
r `  n )
) y ) )
>. ) >. }
57 ctopn 13342 . . . . . . . . . 10  class  TopOpen
5816, 57cfv 5271 . . . . . . . . 9  class  ( TopOpen `  ndx )
5929ccnv 4704 . . . . . . . . . . . . 13  class  `' ( g `  n )
60 vs . . . . . . . . . . . . . 14  set  s
6160cv 1631 . . . . . . . . . . . . 13  class  s
6259, 61cima 4708 . . . . . . . . . . . 12  class  ( `' ( g `  n
) " s )
6337, 57cfv 5271 . . . . . . . . . . . 12  class  ( TopOpen `  ( r `  n
) )
6462, 63wcel 1696 . . . . . . . . . . 11  wff  ( `' ( g `  n
) " s )  e.  ( TopOpen `  (
r `  n )
)
6564, 23, 24wral 2556 . . . . . . . . . 10  wff  A. n  e.  NN  ( `' ( g `  n )
" s )  e.  ( TopOpen `  ( r `  n ) )
6619cpw 3638 . . . . . . . . . 10  class  ~P v
6765, 60, 66crab 2560 . . . . . . . . 9  class  { s  e.  ~P v  | 
A. n  e.  NN  ( `' ( g `  n ) " s
)  e.  ( TopOpen `  ( r `  n
) ) }
6858, 67cop 3656 . . . . . . . 8  class  <. ( TopOpen
`  ndx ) ,  {
s  e.  ~P v  |  A. n  e.  NN  ( `' ( g `  n ) " s
)  e.  ( TopOpen `  ( r `  n
) ) } >.
69 cds 13233 . . . . . . . . . 10  class  dist
7016, 69cfv 5271 . . . . . . . . 9  class  ( dist `  ndx )
7127, 29cfv 5271 . . . . . . . . . . . . 13  class  ( ( g `  n ) `
 n )
7271cdm 4705 . . . . . . . . . . . 12  class  dom  (
( g `  n
) `  n )
7337, 69cfv 5271 . . . . . . . . . . . . . 14  class  ( dist `  ( r `  n
) )
7431, 33, 73co 5874 . . . . . . . . . . . . 13  class  ( x ( dist `  (
r `  n )
) y )
7535, 74cop 3656 . . . . . . . . . . . 12  class  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( x ( dist `  (
r `  n )
) y ) >.
7625, 26, 72, 72, 75cmpt2 5876 . . . . . . . . . . 11  class  ( x  e.  dom  ( ( g `  n ) `
 n ) ,  y  e.  dom  (
( g `  n
) `  n )  |-> 
<. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( x (
dist `  ( r `  n ) ) y ) >. )
7776crn 4706 . . . . . . . . . 10  class  ran  (
x  e.  dom  (
( g `  n
) `  n ) ,  y  e.  dom  ( ( g `  n ) `  n
)  |->  <. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( x (
dist `  ( r `  n ) ) y ) >. )
7823, 24, 77ciun 3921 . . . . . . . . 9  class  U_ n  e.  NN  ran  ( x  e.  dom  ( ( g `  n ) `
 n ) ,  y  e.  dom  (
( g `  n
) `  n )  |-> 
<. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( x (
dist `  ( r `  n ) ) y ) >. )
7970, 78cop 3656 . . . . . . . 8  class  <. ( dist `  ndx ) , 
U_ n  e.  NN  ran  ( x  e.  dom  ( ( g `  n ) `  n
) ,  y  e. 
dom  ( ( g `
 n ) `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( x ( dist `  (
r `  n )
) y ) >.
) >.
80 cple 13231 . . . . . . . . . 10  class  le
8116, 80cfv 5271 . . . . . . . . 9  class  ( le
`  ndx )
8237, 80cfv 5271 . . . . . . . . . . . 12  class  ( le
`  ( r `  n ) )
8382, 29ccom 4709 . . . . . . . . . . 11  class  ( ( le `  ( r `
 n ) )  o.  ( g `  n ) )
8459, 83ccom 4709 . . . . . . . . . 10  class  ( `' ( g `  n
)  o.  ( ( le `  ( r `
 n ) )  o.  ( g `  n ) ) )
8523, 24, 84ciun 3921 . . . . . . . . 9  class  U_ n  e.  NN  ( `' ( g `  n )  o.  ( ( le
`  ( r `  n ) )  o.  ( g `  n
) ) )
8681, 85cop 3656 . . . . . . . 8  class  <. ( le `  ndx ) , 
U_ n  e.  NN  ( `' ( g `  n )  o.  (
( le `  (
r `  n )
)  o.  ( g `
 n ) ) ) >.
8768, 79, 86ctp 3655 . . . . . . 7  class  { <. (
TopOpen `  ndx ) ,  { s  e.  ~P v  |  A. n  e.  NN  ( `' ( g `  n )
" s )  e.  ( TopOpen `  ( r `  n ) ) }
>. ,  <. ( dist `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( ( g `  n ) `  n
) ,  y  e. 
dom  ( ( g `
 n ) `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( x ( dist `  (
r `  n )
) y ) >.
) >. ,  <. ( le `  ndx ) , 
U_ n  e.  NN  ( `' ( g `  n )  o.  (
( le `  (
r `  n )
)  o.  ( g `
 n ) ) ) >. }
8856, 87cun 3163 . . . . . 6  class  ( {
<. ( Base `  ndx ) ,  v >. , 
<. ( +g  `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( g `
 n ) ,  y  e.  dom  (
g `  n )  |-> 
<. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( ( g `
 n ) `  ( x ( +g  `  ( r `  n
) ) y ) ) >. ) >. ,  <. ( .r `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( .r `  (
r `  n )
) y ) )
>. ) >. }  u.  { <. ( TopOpen `  ndx ) ,  { s  e.  ~P v  |  A. n  e.  NN  ( `' ( g `  n )
" s )  e.  ( TopOpen `  ( r `  n ) ) }
>. ,  <. ( dist `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( ( g `  n ) `  n
) ,  y  e. 
dom  ( ( g `
 n ) `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( x ( dist `  (
r `  n )
) y ) >.
) >. ,  <. ( le `  ndx ) , 
U_ n  e.  NN  ( `' ( g `  n )  o.  (
( le `  (
r `  n )
)  o.  ( g `
 n ) ) ) >. } )
8913, 15, 88csb 3094 . . . . 5  class  [_ ( 2nd `  e )  / 
g ]_ ( { <. (
Base `  ndx ) ,  v >. ,  <. ( +g  `  ndx ) , 
U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( +g  `  ( r `
 n ) ) y ) ) >.
) >. ,  <. ( .r `  ndx ) , 
U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( .r `  (
r `  n )
) y ) )
>. ) >. }  u.  { <. ( TopOpen `  ndx ) ,  { s  e.  ~P v  |  A. n  e.  NN  ( `' ( g `  n )
" s )  e.  ( TopOpen `  ( r `  n ) ) }
>. ,  <. ( dist `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( ( g `  n ) `  n
) ,  y  e. 
dom  ( ( g `
 n ) `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( x ( dist `  (
r `  n )
) y ) >.
) >. ,  <. ( le `  ndx ) , 
U_ n  e.  NN  ( `' ( g `  n )  o.  (
( le `  (
r `  n )
)  o.  ( g `
 n ) ) ) >. } )
909, 12, 89csb 3094 . . . 4  class  [_ ( 1st `  e )  / 
v ]_ [_ ( 2nd `  e )  /  g ]_ ( { <. ( Base `  ndx ) ,  v >. ,  <. ( +g  `  ndx ) , 
U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( +g  `  ( r `
 n ) ) y ) ) >.
) >. ,  <. ( .r `  ndx ) , 
U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( .r `  (
r `  n )
) y ) )
>. ) >. }  u.  { <. ( TopOpen `  ndx ) ,  { s  e.  ~P v  |  A. n  e.  NN  ( `' ( g `  n )
" s )  e.  ( TopOpen `  ( r `  n ) ) }
>. ,  <. ( dist `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( ( g `  n ) `  n
) ,  y  e. 
dom  ( ( g `
 n ) `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( x ( dist `  (
r `  n )
) y ) >.
) >. ,  <. ( le `  ndx ) , 
U_ n  e.  NN  ( `' ( g `  n )  o.  (
( le `  (
r `  n )
)  o.  ( g `
 n ) ) ) >. } )
915, 8, 90csb 3094 . . 3  class  [_ ( HomLimB  `  f )  /  e ]_ [_ ( 1st `  e
)  /  v ]_ [_ ( 2nd `  e
)  /  g ]_ ( { <. ( Base `  ndx ) ,  v >. , 
<. ( +g  `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( g `
 n ) ,  y  e.  dom  (
g `  n )  |-> 
<. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( ( g `
 n ) `  ( x ( +g  `  ( r `  n
) ) y ) ) >. ) >. ,  <. ( .r `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( .r `  (
r `  n )
) y ) )
>. ) >. }  u.  { <. ( TopOpen `  ndx ) ,  { s  e.  ~P v  |  A. n  e.  NN  ( `' ( g `  n )
" s )  e.  ( TopOpen `  ( r `  n ) ) }
>. ,  <. ( dist `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( ( g `  n ) `  n
) ,  y  e. 
dom  ( ( g `
 n ) `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( x ( dist `  (
r `  n )
) y ) >.
) >. ,  <. ( le `  ndx ) , 
U_ n  e.  NN  ( `' ( g `  n )  o.  (
( le `  (
r `  n )
)  o.  ( g `
 n ) ) ) >. } )
922, 3, 4, 4, 91cmpt2 5876 . 2  class  ( r  e.  _V ,  f  e.  _V  |->  [_ ( HomLimB  `  f )  /  e ]_ [_ ( 1st `  e
)  /  v ]_ [_ ( 2nd `  e
)  /  g ]_ ( { <. ( Base `  ndx ) ,  v >. , 
<. ( +g  `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( g `
 n ) ,  y  e.  dom  (
g `  n )  |-> 
<. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( ( g `
 n ) `  ( x ( +g  `  ( r `  n
) ) y ) ) >. ) >. ,  <. ( .r `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( .r `  (
r `  n )
) y ) )
>. ) >. }  u.  { <. ( TopOpen `  ndx ) ,  { s  e.  ~P v  |  A. n  e.  NN  ( `' ( g `  n )
" s )  e.  ( TopOpen `  ( r `  n ) ) }
>. ,  <. ( dist `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( ( g `  n ) `  n
) ,  y  e. 
dom  ( ( g `
 n ) `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( x ( dist `  (
r `  n )
) y ) >.
) >. ,  <. ( le `  ndx ) , 
U_ n  e.  NN  ( `' ( g `  n )  o.  (
( le `  (
r `  n )
)  o.  ( g `
 n ) ) ) >. } ) )
931, 92wceq 1632 1  wff HomLim  =  ( r  e.  _V , 
f  e.  _V  |->  [_ ( HomLimB  `  f )  / 
e ]_ [_ ( 1st `  e )  /  v ]_ [_ ( 2nd `  e
)  /  g ]_ ( { <. ( Base `  ndx ) ,  v >. , 
<. ( +g  `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( g `
 n ) ,  y  e.  dom  (
g `  n )  |-> 
<. <. ( ( g `
 n ) `  x ) ,  ( ( g `  n
) `  y ) >. ,  ( ( g `
 n ) `  ( x ( +g  `  ( r `  n
) ) y ) ) >. ) >. ,  <. ( .r `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( g `  n
) ,  y  e. 
dom  ( g `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( ( g `  n
) `  ( x
( .r `  (
r `  n )
) y ) )
>. ) >. }  u.  { <. ( TopOpen `  ndx ) ,  { s  e.  ~P v  |  A. n  e.  NN  ( `' ( g `  n )
" s )  e.  ( TopOpen `  ( r `  n ) ) }
>. ,  <. ( dist `  ndx ) ,  U_ n  e.  NN  ran  ( x  e.  dom  ( ( g `  n ) `  n
) ,  y  e. 
dom  ( ( g `
 n ) `  n )  |->  <. <. (
( g `  n
) `  x ) ,  ( ( g `
 n ) `  y ) >. ,  ( x ( dist `  (
r `  n )
) y ) >.
) >. ,  <. ( le `  ndx ) , 
U_ n  e.  NN  ( `' ( g `  n )  o.  (
( le `  (
r `  n )
)  o.  ( g `
 n ) ) ) >. } ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator