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.Order.Hom.Esakia #3108

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat: port Topology.Order.Hom.Esakia #3108

wants to merge 15 commits into from

Commits on Mar 26, 2023

  1. feat: port Topology.Order.Hom.Esakia

    @urkud
    urkud committed Mar 26, 2023
    Configuration menu
    Copy the full SHA
    8760a42 View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @urkud
    urkud committed Mar 26, 2023
    Configuration menu
    Copy the full SHA
    b099929 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
    @urkud
    urkud committed Mar 26, 2023
    Configuration menu
    Copy the full SHA
    7bfd513 View commit details
    Browse the repository at this point in the history

  4. Partially fix

    @urkud
    urkud committed Mar 26, 2023
    Configuration menu
    Copy the full SHA
    e256de4 View commit details
    Browse the repository at this point in the history

Commits on May 6, 2023

  1. Merge branch 'master' into port/Topology.Order.Hom.Esakia

    @int-y1
    int-y1 committed May 6, 2023
    Configuration menu
    Copy the full SHA
    5dddfd4 View commit details
    Browse the repository at this point in the history

  2. fix

    @int-y1
    int-y1 committed May 6, 2023
    Configuration menu
    Copy the full SHA
    7498739 View commit details
    Browse the repository at this point in the history

  3. code style

    @int-y1
    int-y1 committed May 6, 2023
    Configuration menu
    Copy the full SHA
    8a83142 View commit details
    Browse the repository at this point in the history

  4. docs

    @int-y1
    int-y1 committed May 6, 2023
    Configuration menu
    Copy the full SHA
    a93e398 View commit details
    Browse the repository at this point in the history

  5. uncomment instance

    @int-y1
    int-y1 committed May 6, 2023
    Configuration menu
    Copy the full SHA
    7af4414 View commit details
    Browse the repository at this point in the history

Commits on Jun 4, 2023

  1. Merge branch 'master' into port/Topology.Order.Hom.Esakia

    @mattrobball
    mattrobball committed Jun 4, 2023
    Configuration menu
    Copy the full SHA
    0f7221e View commit details
    Browse the repository at this point in the history

Commits on Jun 5, 2023

  1. Merge branch 'master' into port/Topology.Order.Hom.Esakia

    @mattrobball
    mattrobball committed Jun 5, 2023
    Configuration menu
    Copy the full SHA
    e6eefa0 View commit details
    Browse the repository at this point in the history

  2. reorder theorems to appease simpNF linter

    @mattrobball
    mattrobball committed Jun 5, 2023
    Configuration menu
    Copy the full SHA
    3eaa079 View commit details
    Browse the repository at this point in the history

Commits on Jun 6, 2023

  1. Merge branch 'master' into port/Topology.Order.Hom.Esakia

    @mattrobball
    mattrobball committed Jun 6, 2023
    Configuration menu
    Copy the full SHA
    87c9262 View commit details
    Browse the repository at this point in the history

  2. rework coercion 

    the coercion from EsakiaHom to ContinuousOrderHom was an odd duck
compared to the similar ones in this file. The ContinuousOrderHom
constructor was directly exposed in the coercise resulting in simp
rewriting the fields and simpNF complaining. Introduced
EsakiaHomClass.toContinuousOrderHom which wrapped this constructor
and things behave uniformly.
    @mattrobball
    mattrobball committed Jun 6, 2023
    Configuration menu
    Copy the full SHA
    7ef7c3f View commit details
    Browse the repository at this point in the history

  3. add some porting notes

    @mattrobball
    mattrobball committed Jun 6, 2023
    Configuration menu
    Copy the full SHA
    dc1fee5 View commit details
    Browse the repository at this point in the history