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(Topology/Separation): define R₁ spaces, review API #10085

Closed
wants to merge 18 commits into from
Closed

[Merged by Bors] - feat(Topology/Separation): define R₁ spaces, review API #10085

wants to merge 18 commits into from

Commits on Jan 28, 2024

  1. Snapshot

    @urkud
    urkud committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    948d3c9 View commit details
    Browse the repository at this point in the history

  2. Snapshot

    @urkud
    urkud committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    0338d0e View commit details
    Browse the repository at this point in the history

  3. Snapshot

    @urkud
    urkud committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    6d40163 View commit details
    Browse the repository at this point in the history

  4. Whitespace

    @urkud
    urkud committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    8dda522 View commit details
    Browse the repository at this point in the history

  5. Restore some old names (with @[deprecated])

    @urkud
    urkud committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    dd1dcd4 View commit details
    Browse the repository at this point in the history

  6. Add instances

    @urkud
    urkud committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    d08ef0b View commit details
    Browse the repository at this point in the history

  7. Migrate from deprecated names

    @urkud
    urkud committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    a45ad21 View commit details
    Browse the repository at this point in the history

  8. Fix typos, add to the module docstring

    @urkud
    urkud committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    981bf92 View commit details
    Browse the repository at this point in the history

  9. Drop some unused haves and assumptions

    @urkud
    urkud committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    40f98b3 View commit details
    Browse the repository at this point in the history

Commits on Jan 29, 2024

  1. Merge branch 'master' into YK-R1

    @urkud
    urkud committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    c94a8a7 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/staging' into YK-R1

    @urkud
    urkud committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    22d434f View commit details
    Browse the repository at this point in the history

  3. Apply suggestions from code review 

    Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @urkud @sgouezel
    urkud and sgouezel committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    2e2860c View commit details
    Browse the repository at this point in the history

  4. preregular -> R₁, add deprecation dates

    @urkud
    urkud committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    d1258cb View commit details
    Browse the repository at this point in the history

  5. Search for T[2₂].*\<or\>, edit

    @urkud
    urkud committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    11fe8b1 View commit details
    Browse the repository at this point in the history

  6. Fix docs, add a lemma

    @urkud
    urkud committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    5429407 View commit details
    Browse the repository at this point in the history

  7. "the", newlines

    @urkud
    urkud committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    2a09194 View commit details
    Browse the repository at this point in the history

  8. Migrate from deprecated lemmas

    @urkud
    urkud committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    f57c526 View commit details
    Browse the repository at this point in the history

  9. Update Mathlib/Topology/Separation.lean 

    Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
    @urkud @Parcly-Taxel
    urkud and Parcly-Taxel committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    40b5aff View commit details
    Browse the repository at this point in the history