Skip to content
Snippets Groups Projects

Improve `bijective_finite`.

Merged Improve `bijective_finite`.
robbert/bijective_finite into master
All threads resolved!
Merged Robbert Krebbers requested to merge robbert/bijective_finite into master
All threads resolved!

Make the statement stronger by no longer requiring an inverse.

Make the implementation more efficient by not filtering duplicates.

Merge request reports

Merge request pipeline #79347 passed

Stage: build

Merge request pipeline passed for 9a50355b

Approval is optional

Merged by Robbert KrebbersRobbert Krebbers 2 years ago (Mar 19, 2023 6:21pm UTC)

Merge details

  • Changes merged into with 3af97445.
  • Deleted the source branch.

Pipeline #79349 passed

Stage: build

Pipeline passed for 3af97445 on master

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Ralf Jung
  • Ralf Jung
    Ralf Jung @jung
    Owner

    LGTM with the typos fixed.

  • Robbert Krebbers added 1 commit

    added 1 commit

    Compare with previous version

  • Robbert Krebbers resolved all threads

    resolved all threads

  • Robbert Krebbers enabled an automatic merge when the pipeline for 7d6828b1 succeeds

    enabled an automatic merge when the pipeline for 7d6828b1 succeeds

  • Robbert Krebbers canceled the automatic merge

    canceled the automatic merge

  • Robbert Krebbers added 11 commits

    added 11 commits

    Compare with previous version

    Toggle commit list
  • Robbert Krebbers enabled an automatic merge when the pipeline for 9a50355b succeeds

    enabled an automatic merge when the pipeline for 9a50355b succeeds

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers
    Author Owner

    @iris-users This is a potential breaking change:

    • Improve bijective_finite: do not require an inverse (i.e., have Surj instead of Cancel as premise).
  • Robbert Krebbers mentioned in commit 3af97445

    mentioned in commit 3af97445

  • Robbert Krebbers merged

    merged

    • Please register or sign in to reply