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/continuous_function): lemmas about pointwise sup/inf #7249

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat(topology/continuous_function): lemmas about pointwise sup/inf #7249

wants to merge 6 commits into from

Commits on Apr 18, 2021

  1. feat(topology/continuous_function): lemmas about pointwise sup/inf

    @kim-em
    kim-em committed Apr 18, 2021
    Configuration menu
    Copy the full SHA
    8a371e4 View commit details
    Browse the repository at this point in the history

  2. lint

    @kim-em
    kim-em committed Apr 18, 2021
    Configuration menu
    Copy the full SHA
    7cb67d1 View commit details
    Browse the repository at this point in the history

Commits on Apr 20, 2021

  1. Apply suggestions from code review 

    Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @kim-em @gebner @eric-wieser
    3 people authored Apr 20, 2021
    Configuration menu
    Copy the full SHA
    5e8deac View commit details
    Browse the repository at this point in the history

Commits on Apr 22, 2021

  1. Merge remote-tracking branch 'origin/master' into cf_sup

    @kim-em
    kim-em committed Apr 22, 2021
    Configuration menu
    Copy the full SHA
    ca613ab View commit details
    Browse the repository at this point in the history

  2. use eric's suggestion

    @kim-em
    kim-em committed Apr 22, 2021
    Configuration menu
    Copy the full SHA
    e3ef8b1 View commit details
    Browse the repository at this point in the history

  3. lint

    @kim-em
    kim-em committed Apr 22, 2021
    Configuration menu
    Copy the full SHA
    fe2ff10 View commit details
    Browse the repository at this point in the history