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] - feat(Order/SuccPred): BddAbove.exists_isGreatest_of_nonempty #15944

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat(Order/SuccPred): BddAbove.exists_isGreatest_of_nonempty #15944

wants to merge 6 commits into from

Commits on Aug 18, 2024

  1. feat(Order/SuccPred): BddAbove.exists_isGreatest_of_nonempty 

    when `IsSuccArchimedean`
    @pechersky
    pechersky committed Aug 18, 2024
    Configuration menu
    Copy the full SHA
    eb3c183 View commit details
    Browse the repository at this point in the history

Commits on Aug 27, 2024

  1. Merge branch 'master' into pechersky/bddabove-exists-is-greatest-succ… 

    …arch
    @pechersky
    pechersky committed Aug 27, 2024
    Configuration menu
    Copy the full SHA
    5dd72ee View commit details
    Browse the repository at this point in the history

  2. linear order now necessary

    @pechersky
    pechersky committed Aug 27, 2024
    Configuration menu
    Copy the full SHA
    7642ea1 View commit details
    Browse the repository at this point in the history

Commits on Sep 8, 2024

  1. Merge branch 'master' into pechersky/bddabove-exists-is-greatest-succ… 

    …arch
    @pechersky
    pechersky committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    4310bdc View commit details
    Browse the repository at this point in the history

Commits on Sep 17, 2024

  1. Merge branch 'master' into pechersky/bddabove-exists-is-greatest-succ… 

    …arch
    @pechersky
    pechersky committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    bed7cd9 View commit details
    Browse the repository at this point in the history

Commits on Oct 8, 2024

  1. Update Mathlib/Order/SuccPred/Archimedean.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @pechersky @YaelDillies
    pechersky and YaelDillies authored Oct 8, 2024
    Configuration menu
    Copy the full SHA
    9a9e559 View commit details
    Browse the repository at this point in the history