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(analysis/normed_space/operator_norm): generalize to seminormed space #7202

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat(analysis/normed_space/operator_norm): generalize to seminormed space #7202

wants to merge 10 commits into from

Commits on Apr 15, 2021

  1. feat(analysis/normed_space/operator_norm): generalize to seminormed s… 

    …pace
    @riccardobrasca
    riccardobrasca committed Apr 15, 2021
    Configuration menu
    Copy the full SHA
    d56498c View commit details
    Browse the repository at this point in the history

  2. long line

    @riccardobrasca
    riccardobrasca committed Apr 15, 2021
    Configuration menu
    Copy the full SHA
    4c5ce93 View commit details
    Browse the repository at this point in the history

  3. use pi_semi_norm_le_iff

    @riccardobrasca
    riccardobrasca committed Apr 15, 2021
    Configuration menu
    Copy the full SHA
    d5182b4 View commit details
    Browse the repository at this point in the history

  4. lean needs help here

    @riccardobrasca
    riccardobrasca committed Apr 15, 2021
    Configuration menu
    Copy the full SHA
    c40f26a View commit details
    Browse the repository at this point in the history

  5. for some reason this more general version works, while without semino… 

    …rmed it doesn't
    @riccardobrasca
    riccardobrasca committed Apr 15, 2021
    Configuration menu
    Copy the full SHA
    3c929fe View commit details
    Browse the repository at this point in the history

  6. I don't know why this is needed

    @riccardobrasca
    riccardobrasca committed Apr 15, 2021
    Configuration menu
    Copy the full SHA
    4371580 View commit details
    Browse the repository at this point in the history

  7. Update src/analysis/normed_space/operator_norm.lean 

    Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
    @riccardobrasca @semorrison
    riccardobrasca and semorrison committed Apr 15, 2021
    Configuration menu
    Copy the full SHA
    bd3d091 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'operator_seminorm' of github.com:leanprover-community/m… 

    …athlib into operator_seminorm
    @riccardobrasca
    riccardobrasca committed Apr 15, 2021
    Configuration menu
    Copy the full SHA
    ff5cd58 View commit details
    Browse the repository at this point in the history

Commits on Apr 16, 2021

  1. reorganize the file

    @riccardobrasca
    riccardobrasca committed Apr 16, 2021
    Configuration menu
    Copy the full SHA
    6b121f0 View commit details
    Browse the repository at this point in the history

Commits on Apr 17, 2021

  1. oooops

    @riccardobrasca
    riccardobrasca committed Apr 17, 2021
    Configuration menu
    Copy the full SHA
    6f237e3 View commit details
    Browse the repository at this point in the history