Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged #18990

Closed
wants to merge 21 commits into from
Closed

[Merged by Bors] - feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged #18990

wants to merge 21 commits into from

Commits on May 11, 2023

  1. feat(analysis/normed_space/basic): diameter of scaled sets

    @eric-wieser
    eric-wieser committed May 11, 2023
    Configuration menu
    Copy the full SHA
    5c80b79 View commit details
    Browse the repository at this point in the history

  2. empty commit to re-run CI

    @eric-wieser
    eric-wieser committed May 11, 2023
    Configuration menu
    Copy the full SHA
    6555cdc View commit details
    Browse the repository at this point in the history

  3. basic pointwise lemmas

    @eric-wieser
    eric-wieser committed May 11, 2023
    Configuration menu
    Copy the full SHA
    08ad839 View commit details
    Browse the repository at this point in the history

  4. one more lemma

    @eric-wieser
    eric-wieser committed May 11, 2023
    Configuration menu
    Copy the full SHA
    0a19088 View commit details
    Browse the repository at this point in the history

  5. move to pointwise

    @eric-wieser
    eric-wieser committed May 11, 2023
    Configuration menu
    Copy the full SHA
    9ffde0d View commit details
    Browse the repository at this point in the history

  6. one more lemma

    @eric-wieser
    eric-wieser committed May 11, 2023
    Configuration menu
    Copy the full SHA
    d4fb60f View commit details
    Browse the repository at this point in the history

  7. tidy

    @eric-wieser
    eric-wieser committed May 11, 2023
    Configuration menu
    Copy the full SHA
    f43e754 View commit details
    Browse the repository at this point in the history

  8. lintfix

    @eric-wieser
    eric-wieser committed May 11, 2023
    Configuration menu
    Copy the full SHA
    8a0b671 View commit details
    Browse the repository at this point in the history

  9. one more

    @eric-wieser
    eric-wieser committed May 11, 2023
    Configuration menu
    Copy the full SHA
    3b9a1bb View commit details
    Browse the repository at this point in the history

Commits on May 17, 2023

  1. golf using simpa

    @eric-wieser
    eric-wieser committed May 17, 2023
    Configuration menu
    Copy the full SHA
    28bcbba View commit details
    Browse the repository at this point in the history

  2. helper lemma

    @eric-wieser
    eric-wieser committed May 17, 2023
    Configuration menu
    Copy the full SHA
    6df30f7 View commit details
    Browse the repository at this point in the history

  3. protected

    @eric-wieser
    eric-wieser committed May 17, 2023
    Configuration menu
    Copy the full SHA
    6664162 View commit details
    Browse the repository at this point in the history

  4. use rwa instead

    @eric-wieser
    eric-wieser committed May 17, 2023
    Configuration menu
    Copy the full SHA
    15b686b View commit details
    Browse the repository at this point in the history

  5. one more lemma

    @eric-wieser
    eric-wieser committed May 17, 2023
    Configuration menu
    Copy the full SHA
    c32b039 View commit details
    Browse the repository at this point in the history

  6. revert non-smul changes

    @eric-wieser
    eric-wieser committed May 17, 2023
    Configuration menu
    Copy the full SHA
    672c1c4 View commit details
    Browse the repository at this point in the history

Commits on May 19, 2023

  1. Update src/topology/metric_space/hausdorff_distance.lean 

    Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
    @eric-wieser @YaelDillies
    eric-wieser and YaelDillies authored May 19, 2023
    Configuration menu
    Copy the full SHA
    945e908 View commit details
    Browse the repository at this point in the history

Commits on May 23, 2023

  1. Merge remote-tracking branch 'origin/staging' into eric-wieser/diam-smul

    @eric-wieser
    eric-wieser committed May 23, 2023
    Configuration menu
    Copy the full SHA
    923843c View commit details
    Browse the repository at this point in the history

  2. add missing lemma, force build to fail to get a quick cache:

    @eric-wieser
    eric-wieser committed May 23, 2023
    Configuration menu
    Copy the full SHA
    8d0abaa View commit details
    Browse the repository at this point in the history

  3. fix

    @eric-wieser
    eric-wieser committed May 23, 2023
    Configuration menu
    Copy the full SHA
    0a35f4c View commit details
    Browse the repository at this point in the history

  4. tidy

    @eric-wieser
    eric-wieser committed May 23, 2023
    Configuration menu
    Copy the full SHA
    6cad8f3 View commit details
    Browse the repository at this point in the history

  5. generalize some results

    @eric-wieser
    eric-wieser committed May 23, 2023
    Configuration menu
    Copy the full SHA
    8fa1a57 View commit details
    Browse the repository at this point in the history