fogti/diskr-Wrela
1
0
Fork 1
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
No description
22 commits 1 branch 0 tags 67 KiB
Lean 100%
Find a file
iacore 41214b09c1 mostly clean up (#1) 
I must say I don't know what are you doing with margins_eq

Lean's `Set` doesn't have cardinality (if that's what you mean by "size")

Co-authored-by: iacore <noreply+gpg-stub@1a-insec.net>
Reviewed-on: https://git.exozy.me///fogti/diskr-Wrela/pulls/1
Co-authored-by: iacore <iacore@noreply.git.exozy.me>
Co-committed-by: iacore <iacore@noreply.git.exozy.me>
2024-08-09 16:52:24 +00:00
.gitignore +lake stuff 2024-08-06 22:06:36 +02:00
DiskrWrela.lean mostly clean up (#1) 2024-08-09 16:52:24 +00:00
lake-manifest.json try to formulate main progress theorem 2024-08-06 23:08:38 +02:00
lakefile.lean mostly clean up (#1) 2024-08-09 16:52:24 +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?