add few finite map theorems

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

https://hol-theorem-prover.org

Other

606 stars 132 forks source link

add few finite map theorems #1202

Closed rsoeldner closed 4 months ago

rsoeldner commented 4 months ago

While working on my formalisation, I encountered these theorems which I believe might be useful. Not sure about the process, I'm keen to feedback.

mn200 commented 4 months ago

Looks good; thanks!