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

feat:(Combinatorics/SimpleGraph): connected SimpleGraph forms a MetricSpace #14715

Closed
wants to merge 16 commits into from
Closed

feat:(Combinatorics/SimpleGraph): connected SimpleGraph forms a MetricSpace #14715

wants to merge 16 commits into from

Commits on Jul 1, 2024

  1. not_reachable_iff_Walk_isEmpty

    @Rida-Hamadani
    Rida-Hamadani committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    0d28e97 View commit details
    Browse the repository at this point in the history

Commits on Jul 9, 2024

  1. init

    @Rida-Hamadani
    Rida-Hamadani committed Jul 9, 2024
    Configuration menu
    Copy the full SHA
    401005c View commit details
    Browse the repository at this point in the history

  2. provide API for dist 

    co-authored-by: Bhavik Mehta <[email protected]>
    @Rida-Hamadani
    Rida-Hamadani committed Jul 9, 2024
    Configuration menu
    Copy the full SHA
    353eb9c View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into rida/refactorDist

    @Rida-Hamadani
    Rida-Hamadani authored Jul 9, 2024
    Configuration menu
    Copy the full SHA
    034f3b8 View commit details
    Browse the repository at this point in the history

  4. fixes

    @Rida-Hamadani
    Rida-Hamadani committed Jul 9, 2024
    Configuration menu
    Copy the full SHA
    1996e74 View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2024

  1. prove iInf_eq_zero

    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    ff344f9 View commit details
    Browse the repository at this point in the history

  2. docs and implicit params

    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    033d3d9 View commit details
    Browse the repository at this point in the history

  3. remove duplicate

    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    aff9421 View commit details
    Browse the repository at this point in the history

  4. use naming convention

    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    fa54c4a View commit details
    Browse the repository at this point in the history

  5. Apply suggestions from review. 

    co-authored-by: Kyle Miller <[email protected]>
    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    0a60d79 View commit details
    Browse the repository at this point in the history

  6. revert unwanted naming changes

    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    7024912 View commit details
    Browse the repository at this point in the history

  7. Apply changes from review. 

    co-authered-by: Bhavik Mehta <[email protected]>
    @Rida-Hamadani
    Rida-Hamadani committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    7d8a20b View commit details
    Browse the repository at this point in the history

Commits on Jul 11, 2024

  1. Apply suggestions from review. 

    co-authored-by: Bhavik Mehta
co-authored-by: Kyle Miller
    @Rida-Hamadani
    Rida-Hamadani committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    f59304b View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Combinatorics/SimpleGraph/Metric.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @Rida-Hamadani @github-actions
    Rida-Hamadani and github-actions[bot] authored Jul 11, 2024
    Configuration menu
    Copy the full SHA
    183bcdd View commit details
    Browse the repository at this point in the history

Commits on Jul 13, 2024

  1. feat: connected graph forms a metric space

    @Rida-Hamadani
    Rida-Hamadani committed Jul 13, 2024
    Configuration menu
    Copy the full SHA
    b0d41a2 View commit details
    Browse the repository at this point in the history

  2. remove Verts

    @Rida-Hamadani
    Rida-Hamadani committed Jul 13, 2024
    Configuration menu
    Copy the full SHA
    a9f18ca View commit details
    Browse the repository at this point in the history