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

[Merged by Bors] - feat(topology/metric_space): diameter of pointwise zero and addition #19028

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat(topology/metric_space): diameter of pointwise zero and addition #19028

wants to merge 10 commits into from

Commits on May 17, 2023

  1. feat(topology/metric_space): diameter of pointwise zero and addition 

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

  2. progress

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

  3. helper

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

Commits on Jul 12, 2023

  1. add ediam_image2_le

    @eric-wieser
    eric-wieser committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    54f4671 View commit details
    Browse the repository at this point in the history

  2. golf

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

  3. fix

    @eric-wieser
    eric-wieser committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    316137e View commit details
    Browse the repository at this point in the history

  4. add new results

    @eric-wieser
    eric-wieser committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    7b34024 View commit details
    Browse the repository at this point in the history

Commits on Jul 14, 2023

  1. generalize

    @eric-wieser
    eric-wieser committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    4e21956 View commit details
    Browse the repository at this point in the history

  2. fix

    @eric-wieser
    eric-wieser committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    4065f17 View commit details
    Browse the repository at this point in the history

Commits on Jul 16, 2023

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

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