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 | ⊢ ( 𝑅 BlockLiftMap 𝐴 ) = ( 𝑚 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↦ [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cR | ⊢ 𝑅 | |
| 1 | cA | ⊢ 𝐴 | |
| 2 | 1 0 | cblockliftmap | ⊢ ( 𝑅 BlockLiftMap 𝐴 ) |
| 3 | vm | ⊢ 𝑚 | |
| 4 | cep | ⊢ E | |
| 5 | 4 | ccnv | ⊢ ◡ E |
| 6 | 5 1 | cres | ⊢ ( ◡ E ↾ 𝐴 ) |
| 7 | 0 6 | cxrn | ⊢ ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) |
| 8 | 7 | cdm | ⊢ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) |
| 9 | 3 | cv | ⊢ 𝑚 |
| 10 | 9 7 | cec | ⊢ [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) |
| 11 | 3 8 10 | cmpt | ⊢ ( 𝑚 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↦ [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) |
| 12 | 2 11 | wceq | ⊢ ( 𝑅 BlockLiftMap 𝐴 ) = ( 𝑚 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↦ [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) |