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: Lipschitz extensions of maps into l^infty #5107

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - feat: Lipschitz extensions of maps into l^infty #5107

wants to merge 16 commits into from

Commits on Jun 15, 2023

  1. Lipschitz_ext

    @chriscamano
    chriscamano committed Jun 15, 2023
    Configuration menu
    Copy the full SHA
    6638be9 View commit details
    Browse the repository at this point in the history

  2. Moved lip_const

    @chriscamano
    chriscamano committed Jun 15, 2023
    Configuration menu
    Copy the full SHA
    2c8a90f View commit details
    Browse the repository at this point in the history

  3. fixed line break error

    @chriscamano
    chriscamano committed Jun 15, 2023
    Configuration menu
    Copy the full SHA
    108f22c View commit details
    Browse the repository at this point in the history

  4. fixed doc string

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

Commits on Jun 16, 2023

  1. correct indentation

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

  2. citation

    @chriscamano
    chriscamano committed Jun 16, 2023
    Configuration menu
    Copy the full SHA
    736ad9b View commit details
    Browse the repository at this point in the history

  3. theorem rename

    @chriscamano
    chriscamano committed Jun 16, 2023
    Configuration menu
    Copy the full SHA
    9b23db4 View commit details
    Browse the repository at this point in the history

  4. theorem statement correction

    @chriscamano
    chriscamano committed Jun 16, 2023
    Configuration menu
    Copy the full SHA
    693799f View commit details
    Browse the repository at this point in the history

  5. fixed theorem statement

    @chriscamano
    chriscamano committed Jun 16, 2023
    Configuration menu
    Copy the full SHA
    3f74b0a View commit details
    Browse the repository at this point in the history

  6. added lpinf notation to lp

    @chriscamano
    chriscamano committed Jun 16, 2023
    Configuration menu
    Copy the full SHA
    79778cc View commit details
    Browse the repository at this point in the history

  7. fixed format bib

    @chriscamano
    chriscamano committed Jun 16, 2023
    Configuration menu
    Copy the full SHA
    1ce9f2c View commit details
    Browse the repository at this point in the history

  8. Added Lip lemmas, reduced calc block

    @chriscamano
    chriscamano committed Jun 16, 2023
    Configuration menu
    Copy the full SHA
    f91fae3 View commit details
    Browse the repository at this point in the history

  9. fixed notation port to lip section in lp

    @chriscamano
    chriscamano committed Jun 16, 2023
    1 Configuration menu
    Copy the full SHA
    2a52137 View commit details
    Browse the repository at this point in the history

  10. fixed notation port

    @chriscamano
    chriscamano committed Jun 16, 2023
    Configuration menu
    Copy the full SHA
    ba4c9cd View commit details
    Browse the repository at this point in the history

Commits on Jun 17, 2023

  1. Update Mathlib/Topology/MetricSpace/Kuratowski.lean 

    toms golf

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @chriscamano @tb65536
    chriscamano and tb65536 committed Jun 17, 2023
    Configuration menu
    Copy the full SHA
    521d2a9 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Topology/MetricSpace/Kuratowski.lean 

    Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @chriscamano @tb65536
    chriscamano and tb65536 committed Jun 17, 2023
    Configuration menu
    Copy the full SHA
    6ed96a0 View commit details
    Browse the repository at this point in the history