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: port Topology.TietzeExtension #4246

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat: port Topology.TietzeExtension #4246

wants to merge 14 commits into from

Commits on May 23, 2023

  1. feat: port Topology.TietzeExtension

    @apurvnakade
    apurvnakade committed May 23, 2023
    Configuration menu
    Copy the full SHA
    51f8443 View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @apurvnakade
    apurvnakade committed May 23, 2023
    Configuration menu
    Copy the full SHA
    b782ad9 View commit details
    Browse the repository at this point in the history

  3. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @apurvnakade
    apurvnakade committed May 23, 2023
    Configuration menu
    Copy the full SHA
    876701d View commit details
    Browse the repository at this point in the history

  4. Several fixes

    @apurvnakade
    apurvnakade committed May 23, 2023
    Configuration menu
    Copy the full SHA
    2ecb9e7 View commit details
    Browse the repository at this point in the history

  5. Several fixes

    @apurvnakade
    apurvnakade committed May 23, 2023
    Configuration menu
    Copy the full SHA
    60bc916 View commit details
    Browse the repository at this point in the history

  6. Several fixes

    @apurvnakade
    apurvnakade committed May 23, 2023
    Configuration menu
    Copy the full SHA
    cee53ea View commit details
    Browse the repository at this point in the history

  7. Fixes

    @apurvnakade
    apurvnakade committed May 23, 2023
    Configuration menu
    Copy the full SHA
    9f239c9 View commit details
    Browse the repository at this point in the history

  8. Fix lint error

    @apurvnakade
    apurvnakade committed May 23, 2023
    Configuration menu
    Copy the full SHA
    fa39316 View commit details
    Browse the repository at this point in the history

  9. Fix Coe

    @apurvnakade
    apurvnakade committed May 23, 2023
    Configuration menu
    Copy the full SHA
    93f6047 View commit details
    Browse the repository at this point in the history

  10. Fix exists_extension_forall_mem_of_closedEmbedding

    @apurvnakade
    apurvnakade committed May 23, 2023
    Configuration menu
    Copy the full SHA
    872f93c View commit details
    Browse the repository at this point in the history

  11. set_option maxHeartbeats 0

    @apurvnakade
    apurvnakade committed May 23, 2023
    Configuration menu
    Copy the full SHA
    b6062aa View commit details
    Browse the repository at this point in the history

  12. set_option maxHeartbeats 250000

    @apurvnakade
    apurvnakade committed May 23, 2023
    Configuration menu
    Copy the full SHA
    70e8aec View commit details
    Browse the repository at this point in the history

Commits on May 30, 2023

  1. Merge branch 'master' into port/Topology.TietzeExtension

    @Komyyy
    Komyyy committed May 30, 2023
    Configuration menu
    Copy the full SHA
    a693788 View commit details
    Browse the repository at this point in the history

  2. fix

    @Komyyy
    Komyyy committed May 30, 2023
    Configuration menu
    Copy the full SHA
    3bd1d77 View commit details
    Browse the repository at this point in the history