Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - fix(Data/Set/Image): simp confluence issues with image_subset_iff #8683

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - fix(Data/Set/Image): simp confluence issues with image_subset_iff #8683

wants to merge 11 commits into from

Commits on Nov 28, 2023

  1. fix(Data/Set/Image): simp confluence issues with image_subset_iff 

    `image_subset_iff` is a questionable simp lemma because it converts
an application of image into preimage unconditionally. This means that if any
simp lemma applies to applications of images, there must be a corresponding
lemma for applications of preimage. These lemmas are what I found missing after
loogling.
    @timotree3
    timotree3 committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    c1667b0 View commit details
    Browse the repository at this point in the history

  2. Document confluence issues with explicit tests

    @timotree3
    timotree3 committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    5629828 View commit details
    Browse the repository at this point in the history

  3. fix style

    @timotree3
    timotree3 committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    919ee48 View commit details
    Browse the repository at this point in the history

Commits on Nov 29, 2023

  1. move examples to tests/

    @timotree3
    timotree3 committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    6d70b96 View commit details
    Browse the repository at this point in the history

Commits on Dec 12, 2023

  1. update implicit arguments as recommended in review 

    Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
    @timotree3 @YaelDillies
    timotree3 and YaelDillies committed Dec 12, 2023
    Configuration menu
    Copy the full SHA
    5c73ab3 View commit details
    Browse the repository at this point in the history

Commits on Feb 10, 2024

  1. Merge branch 'master' into TCB/image-subset-confl

    @timotree3
    timotree3 committed Feb 10, 2024
    Configuration menu
    Copy the full SHA
    895522d View commit details
    Browse the repository at this point in the history

  2. add Set.subset_range_of_surjective

    @timotree3
    timotree3 committed Feb 10, 2024
    Configuration menu
    Copy the full SHA
    a050646 View commit details
    Browse the repository at this point in the history

  3. add Set.preimage_eq_univ_iff

    @timotree3
    timotree3 committed Feb 10, 2024
    Configuration menu
    Copy the full SHA
    108a976 View commit details
    Browse the repository at this point in the history

  4. fix simpnf lint

    @timotree3
    timotree3 committed Feb 10, 2024
    Configuration menu
    Copy the full SHA
    8ed6824 View commit details
    Browse the repository at this point in the history

  5. remove spurious newline 

    Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
    @timotree3 @YaelDillies
    timotree3 and YaelDillies committed Feb 10, 2024
    Configuration menu
    Copy the full SHA
    2e991ff View commit details
    Browse the repository at this point in the history

  6. add Finset.univ_subset_iff

    @timotree3
    timotree3 committed Feb 10, 2024
    Configuration menu
    Copy the full SHA
    e0edc8c View commit details
    Browse the repository at this point in the history