[Merged by Bors] - feat(Data/Rel): prove simple propositions about images, preimages and graphs of relations #6559
Conversation
uniwuni
added
the
awaiting-review
jcommelin
added
awaiting-author
simp attributes Co-authored-by: Johan Commelin <johan@commelin.net>
|
Changes should be resolved, I wasn't too sure when to add lemmas of this kind to the default simps |
uniwuni
added
awaiting-review
bors
bot
changed the base branch from
master
to
ScottCarnahan/BinomialRing2
semorrison
changed the base branch from
ScottCarnahan/BinomialRing2
to
master
| rw[←hf.left] | ||
| simp only [forall_eq', and_self] | ||
| · intro h | ||
| rcases Classical.axiomOfChoice (λ x ↦ (h x).exists) with ⟨f,hf⟩ |
There was a problem hiding this comment.
There should probably be an equivalent to the axiom of choice for ExistsUnique.
There was a problem hiding this comment.
oh if only there was, ExistsUnique seems a little underdeveloped when it comes to these things
|
✌️ uniwuni can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
bors r+ |
… graphs of relations (#6559) Add lemmas about relation composition with top and bottom elements, conditions under which images under a relation form the whole codomain, and the equivalence between being a functional relation and representable by the graph of a function. Co-authored-by: uniwuni <95649083+uniwuni@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
Add lemmas about relation composition with top and bottom elements, conditions under which images under a relation form the whole codomain, and the equivalence between being a functional relation and representable by the graph of a function.