Description: The function returning dyadic square covering for a given size has domain ( ran I X. ran I ) . (Contributed by Thierry Arnoux, 19-Sep-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sxbrsiga.0 | |- J = ( topGen ` ran (,) ) |
|
dya2ioc.1 | |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) |
||
dya2ioc.2 | |- R = ( u e. ran I , v e. ran I |-> ( u X. v ) ) |
||
Assertion | dya2iocrfn | |- R Fn ( ran I X. ran I ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sxbrsiga.0 | |- J = ( topGen ` ran (,) ) |
|
2 | dya2ioc.1 | |- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) |
|
3 | dya2ioc.2 | |- R = ( u e. ran I , v e. ran I |-> ( u X. v ) ) |
|
4 | vex | |- u e. _V |
|
5 | vex | |- v e. _V |
|
6 | 4 5 | xpex | |- ( u X. v ) e. _V |
7 | 3 6 | fnmpoi | |- R Fn ( ran I X. ran I ) |