Description: Define the block lift map. Given a relation R and a carrier/set A , we form the block relation ( R |X.`'E ) (i.e., "follow both R and element"), restricted to A (or, equivalently, "follow both R and elements-of-A", cf. xrnres2 ). Then map each domain element m to its coset [ m ] under that restricted block relation.
For m in the domain, which requires ( m e. A /\ m =/= (/) /\ [ m ] R =/= (/) ) (cf. eldmxrncnvepres ), the fiber has the product form [ m ] ( R |X. ``' E ) = ( [ m ] R X. m ) , so the block relation lifts a block m to the rectangular grid "external labels X. ` internal members", see dfblockliftmap2 . Contrast: while the adjoined lift, via ( R u.`' _E ) ` , attaches neighbors and members in a single relation (see dfadjliftmap2 ), the block lift labels each internal member by each external neighbor.
For the general case and a two-stage construction (first block lift, then adjoin membership), see the comments to df-adjliftmap . For the equilibrium condition, see df-blockliftfix and dfblockliftfix2 . (Contributed by Peter Mazsa, 24-Jan-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-blockliftmap | |- ( R BlockLiftMap A ) = ( m e. dom ( R |X. ( `' _E |` A ) ) |-> [ m ] ( R |X. ( `' _E |` A ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cR | |- R |
|
| 1 | cA | |- A |
|
| 2 | 1 0 | cblockliftmap | |- ( R BlockLiftMap A ) |
| 3 | vm | |- m |
|
| 4 | cep | |- _E |
|
| 5 | 4 | ccnv | |- `' _E |
| 6 | 5 1 | cres | |- ( `' _E |` A ) |
| 7 | 0 6 | cxrn | |- ( R |X. ( `' _E |` A ) ) |
| 8 | 7 | cdm | |- dom ( R |X. ( `' _E |` A ) ) |
| 9 | 3 | cv | |- m |
| 10 | 9 7 | cec | |- [ m ] ( R |X. ( `' _E |` A ) ) |
| 11 | 3 8 10 | cmpt | |- ( m e. dom ( R |X. ( `' _E |` A ) ) |-> [ m ] ( R |X. ( `' _E |` A ) ) ) |
| 12 | 2 11 | wceq | |- ( R BlockLiftMap A ) = ( m e. dom ( R |X. ( `' _E |` A ) ) |-> [ m ] ( R |X. ( `' _E |` A ) ) ) |