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

[Merged by Bors] - feat(data/real/basic): add real.supr_nonneg etc #19096

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat(data/real/basic): add real.supr_nonneg etc #19096

wants to merge 3 commits into from

Commits on May 25, 2023

  1. feat(data/real/basic): add real.supr_nonneg etc 

    Motivated by lemmas from the sphere eversion project
    @urkud
    urkud committed May 25, 2023
    Configuration menu
    Copy the full SHA
    3f46aeb View commit details
    Browse the repository at this point in the history

  2. Fix

    @urkud
    urkud committed May 25, 2023
    Configuration menu
    Copy the full SHA
    a94eced View commit details
    Browse the repository at this point in the history

Commits on May 26, 2023

  1. Protect new lemmas

    @urkud
    urkud committed May 26, 2023
    Configuration menu
    Copy the full SHA
    9271baa View commit details
    Browse the repository at this point in the history