GitLab upgrade to version 17.6.2 on Monday (https://go.epfl.ch/CHG0045788) may have caused issues for users using password authentication for git push and similar. If that is your case, and especially if you are in a pinch w.r.t. assignment deadlines, please reach out directly to gitlab-admins@groupes.epfl.ch, Cc 1234@epfl.ch . Meanwhile, you can work around the issue by using an SSH key pair: https://gitlab.epfl.ch/help/user/ssh.md . Watch this space for updates and further instructions.
This PR proves several theorems regarding restricted functions. Notably, it proves the relation domain of a restricted function
relationDomain(restrictedFunction(f, x)) === setIntersection(x, relationDomain(f))
as well as a cancellation theorem:
restrictedFunction(f, relationDomain(f)) === f
that is useful for group theory.
It also contains several tactics imported from the Work-in-Progress on Group Theory (#151), as well as first-order logic lemmas for proving the theorem.
Note that since Definition
tactic uses Tautology
, I placed the tactics in the main submodule instead of SimpleDeducedSteps
.