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 ) |