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: Ordinal Approximants of the least/greatest fixed point in a complete lattice #8996

Closed
wants to merge 32 commits into from
Closed

[Merged by Bors] - feat: Ordinal Approximants of the least/greatest fixed point in a complete lattice #8996

wants to merge 32 commits into from

Commits on Dec 11, 2023

  1. finished proof

    Ira Fesefeldt committed Dec 11, 2023
    Configuration menu
    Copy the full SHA
    dde77d0 View commit details
    Browse the repository at this point in the history

  2. line and characters formatting

    Ira Fesefeldt committed Dec 11, 2023
    Configuration menu
    Copy the full SHA
    f7693cd View commit details
    Browse the repository at this point in the history

  3. linter fixes

    Ira Fesefeldt committed Dec 11, 2023
    Configuration menu
    Copy the full SHA
    d1b3ae4 View commit details
    Browse the repository at this point in the history

  4. deactivate unusredVariables linting

    Ira Fesefeldt committed Dec 11, 2023
    Configuration menu
    Copy the full SHA
    8ff8b17 View commit details
    Browse the repository at this point in the history

  5. made some lemmas to theorems

    Ira Fesefeldt committed Dec 11, 2023
    Configuration menu
    Copy the full SHA
    752d401 View commit details
    Browse the repository at this point in the history

  6. documentation and formatting

    Ira Fesefeldt committed Dec 11, 2023
    Configuration menu
    Copy the full SHA
    a1ef93a View commit details
    Browse the repository at this point in the history

Commits on Mar 2, 2024

  1. Merge branch 'master' into constructive-tk-fixpoint

    Ira Fesefeldt committed Mar 2, 2024
    Configuration menu
    Copy the full SHA
    50e1f62 View commit details
    Browse the repository at this point in the history

  2. review changes

    Ira Fesefeldt committed Mar 2, 2024
    Configuration menu
    Copy the full SHA
    645df67 View commit details
    Browse the repository at this point in the history

  3. fixed multiple typos and overseen issues

    Ira Fesefeldt committed Mar 2, 2024
    Configuration menu
    Copy the full SHA
    32ada0d View commit details
    Browse the repository at this point in the history

  4. fixed linting issues

    Ira Fesefeldt committed Mar 2, 2024
    Configuration menu
    Copy the full SHA
    625d294 View commit details
    Browse the repository at this point in the history

  5. squeezed simps

    Ira Fesefeldt committed Mar 2, 2024
    Configuration menu
    Copy the full SHA
    43e1e61 View commit details
    Browse the repository at this point in the history

  6. references linting and changed year in license

    Ira Fesefeldt committed Mar 2, 2024
    Configuration menu
    Copy the full SHA
    41c79da View commit details
    Browse the repository at this point in the history

Commits on Mar 3, 2024

  1. indeed missed renaming the documentation

    Ira Fesefeldt committed Mar 3, 2024
    Configuration menu
    Copy the full SHA
    8f8f4d4 View commit details
    Browse the repository at this point in the history

  2. changed some of the theorem names

    Ira Fesefeldt committed Mar 3, 2024
    Configuration menu
    Copy the full SHA
    77b2fd8 View commit details
    Browse the repository at this point in the history

Commits on Mar 5, 2024

  1. fixed wrong name

    Ira Fesefeldt committed Mar 5, 2024
    Configuration menu
    Copy the full SHA
    f409434 View commit details
    Browse the repository at this point in the history

Commits on Mar 7, 2024

  1. removed uncessary theorems and fixed documentation

    Ira Fesefeldt committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    951ec45 View commit details
    Browse the repository at this point in the history

Commits on Mar 18, 2024

  1. style and not_injective_iff enhanced

    @PhoenixIra
    PhoenixIra committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    e78b004 View commit details
    Browse the repository at this point in the history

  2. changed limitation to Set.InjOn

    @PhoenixIra
    PhoenixIra committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    a5b9bb2 View commit details
    Browse the repository at this point in the history

  3. pr comments

    @PhoenixIra
    PhoenixIra committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    483c283 View commit details
    Browse the repository at this point in the history

  4. linter

    @PhoenixIra
    PhoenixIra committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    fab0ade View commit details
    Browse the repository at this point in the history

  5. inlined lemma made nicer

    @PhoenixIra
    PhoenixIra committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    378591c View commit details
    Browse the repository at this point in the history

  6. renamed file and changed documentation

    @PhoenixIra
    PhoenixIra committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    27b3b60 View commit details
    Browse the repository at this point in the history

  7. changed file to correct order in Mathlib.lean

    @PhoenixIra
    PhoenixIra committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    204e6ad View commit details
    Browse the repository at this point in the history

  8. make Set defs and lemmas shorter

    @PhoenixIra
    PhoenixIra committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    06e58a4 View commit details
    Browse the repository at this point in the history

  9. made more variables implicit

    @PhoenixIra
    PhoenixIra committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    7af7501 View commit details
    Browse the repository at this point in the history

  10. simplified lfpApprox_eq_of_mem_fixedPoint

    @PhoenixIra
    PhoenixIra committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    2b6c980 View commit details
    Browse the repository at this point in the history

  11. fixed build error

    @PhoenixIra
    PhoenixIra committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    5f89650 View commit details
    Browse the repository at this point in the history

Commits on Apr 9, 2024

  1. review comments

    Ira Fesefeldt committed Apr 9, 2024
    Configuration menu
    Copy the full SHA
    ef44b56 View commit details
    Browse the repository at this point in the history

  2. better documentation

    Ira Fesefeldt committed Apr 9, 2024
    Configuration menu
    Copy the full SHA
    2c609b5 View commit details
    Browse the repository at this point in the history

  3. typos and similiar

    Ira Fesefeldt committed Apr 9, 2024
    Configuration menu
    Copy the full SHA
    42293bb View commit details
    Browse the repository at this point in the history

Commits on Apr 10, 2024

  1. removed init from name

    Ira Fesefeldt committed Apr 10, 2024
    Configuration menu
    Copy the full SHA
    66dd10c View commit details
    Browse the repository at this point in the history

  2. typo

    Ira Fesefeldt committed Apr 10, 2024
    Configuration menu
    Copy the full SHA
    1d00b40 View commit details
    Browse the repository at this point in the history