iacore/diskr-Wrela
1
0
Fork 0
forked from fogti/diskr-Wrela
Code Pull requests Activity
No description
28 commits 1 branch 0 tags 71 KiB
Lean 100%
Find a file
iacore 39abce45b4
++
2024-08-15 22:47:30 +00:00
.gitignore +lake stuff 2024-08-06 22:06:36 +02:00
DiskrWrela.lean ++ 2024-08-15 22:47:30 +00:00
lake-manifest.json try to formulate main progress theorem 2024-08-06 23:08:38 +02:00
lakefile.lean clean up 2024-08-09 15:46:04 +00:00
lean-toolchain try to formulate main progress theorem 2024-08-06 23:08:38 +02:00
README.md initial commit 2024-08-06 08:52:23 +02:00

README.md

diskr-Wrela

Idea: If I have two relations R_1, R_t ∈ A × B where for each A and for each B the amount of elements incident to each one is the same between R_1 and R_2, and I am allowed to construct new relations R_n from R_{n-1} by transforming "aR_{n-1}b, cR_{n-1}d" to "aR_nd, cR_nb", are there any R_1, R_t where R_t can't be reached via such swaps from R_1? How to construct those?